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