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] problem with \old()

On Tue, 09 Nov 2010, Pascal Cuoq wrote:

> On 11/9/10, Nicholas Mc Guire <der.herr at hofr.at> wrote:
> > well I get the same with -val oswell as when running with jessie / alt-ergo
> > so I assumed that is not the cause.
> 
> Yes, the value analysis' weakness when it comes to \old constructs is
> the cause. It just seems that option -users is all the rage these
> days, but it's supposed to be undocumented. This is what I would like
> to fix.

well actually its just the second from the bottom when you type
frama-c -help and as the -users-help seemed like the simplest option (or
actually the one with more or less no options) it made a "obvious" test
target.

> 
> Even if you are interested by both the value analysis and Jessie, I
> would recommend that you use the options in separate invocations of
> Frama-C.
> 
> > the problem with that is that frama-c -jessie inc2.c will try to start the
> > gui - but I can't use the gui so I was trying to get it to work in console
> > mode.
> 
> If you write the following to a C file, you will be able to verify it
> using Jessie in command-line mode:
> 
> 
> /*@ requires \valid(p) ;
>     requires 0 <= *p < 2000000000 ;
>    ensures \old(*p) < *p ;
> */
> void fun(int *p) {
>   unsigned int t=*p;
>   t++;
>   *p=t;
> }
> 
> Use the command-line:
> 
> frama-c -jessie -jessie-atp alt-ergo inc2.c
> 
> You should get:
> 
> (. = valid * = invalid ? = unknown # = timeout ! = failure)
> why/inc2_why.why              : ........ (8/0/0/0/0)
>

ok - that did it for me - I actually had tried that before for my 
example but got 2 unknown as well - and then tried to figure out
where they came from - thanks!
 
> But I used to GUI to understand the missing annotations. I do not know
> how to debug code or specification using only the command-line.
> 
> If you want to remove the 0 <= *p precondition,
> the cast from int to unsigned int can perhaps be handled
> by adding the line:
> 
> #pragma JessieIntegerModel(modulo)
> 
> to the file, but that makes things more complicated for provers.
>
many thanks for your help !

thx!
hofrat