--- layout: fc_discuss_archives title: Message 12 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 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.

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)

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.

Regards,

Pascal