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 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