--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on November 2010 ---
[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