Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Newbie question

Hi,

If you want to learn the Jessie plugin, please use the jessie tutorial 
instead :

  http://frama-c.cea.fr/jessie_tutorial_index.html

The example max_seq given in ACSL tutorial is not annotated properly to 
be proved.

About provers to install on Linux: see the prover tips page of the Why tool.

- Claude


Aaron Rocha wrote:
> Hi everybody, 
>
> I am new to Frama-C and to the world of assisted mathematical proofs. Basically, I am a C developer who is interesting in writing code that can be verified. I ran across Frama-C and it looks like just the type of thing I was looking for. I am having a little bit of a hard time getting started though.
>
> I am on Linux and it looks like only a selected number of proof assistants are available on this platform. It sounds to me as though Coq would be the best one. The problem is that, if I use Coq, I have to actually fill the proof in (after make -f <source file>.makefile coq) and I am not familiar with Coq yet. So I am using Alt-Ergo instead.
>
> But Alt-Ergo fails to prove the preservation of loop invariants in this code from the tutorial:
>
> /*@ requires n > 0; 
>     requires \valid(p+ (0..n-1));
>     assigns \nothing;
>     ensures \forall int i; 0 <= i <= n-1 ==> \result >= p[i]; 
>     ensures \exists int e; 0 <= e <= n-1 &&  \result == p[e]; 
>  */ 
> int max_seq(int* p, int n) {
>
>   int res = *p; 
>   int i   = 0;
>
>   //@ ghost int e = 0;
>   /*@ loop invariant \forall integer j; 0 <= j <= i ==> res >= *(p+j);
>       loop invariant \valid(p+e) && p[e] == res;
>    */
>   for(i = 0; i < n; i++) { 
>     if (res < *p) { 
>        res = *p; 
>        //@ ghost e = i;
>     }
>     p++; 
>   } 
>   return res; 
> } 
>
> Do you run frama-c on Linux? If so, what proof assistants are you using? If Coq is the way to go, is there some sort of gentle introduction on how to use Coq with Frama-c?
>
> Thanks in advance
>
>
>       __________________________________________________________________
> Yahoo! Canada Toolbar: Search from anywhere on the web, and bookmark your favourite sites. Download it now
> http://ca.toolbar.yahoo.com.
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>   


-- 
Claude March?                          | tel: +33 1 72 92 59 69           
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93 
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29   
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |