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