--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on August 2017 ---
2017-08-04 17:50 GMT+02:00 Yifan Lu <me at yifanlu.com>: > Thanks, if I add an assigns and add another point parameter, the > second assert is still not provable > > test.c: > /*@ predicate something(int *x) = \true; */ > > /*@ requires something(x); > @ assigns a[0..7]; > @*/ > int test2(int *x, int a[static 8]); > > /*@ requires *x == 5; > @*/ > int test(int *x, int a[static 8]) { > //@ assert *x == 5; > test2(x, a); > //@ assert *x == 5; > return 0; > } > > Run with "frama-c -wp -wp-rte -wp-split test.c" > > On Fri, Aug 4, 2017 at 12:55 AM, Virgile Prevosto > <virgile.prevosto at m4x.org> wrote: >> Hello, >> >> 2017-08-04 1:53 GMT+02:00 Yifan Lu <me at yifanlu.com>: >>> It appears that if I remove the const >>> >>> extern int * const globalx; >>> extern int * const globaly; >>> >>> I can use -wp-model ref and all is well... >>> >>> but I ran into another problem >>> >>> /*@ predicate something(int *x) = \true; */ >>> >>> /*@ requires something(x); */ >>> int test7(int *x); >>> >>> /*@ requires *x == 5; >>> @*/ >>> int test6(int *x) { >>> //@ assert *x == 5; >>> test7(x); >>> //@ assert *x == 5; >>> return 0; >>> } >>> >>> The second assertion cannot be proved. If I remove the predicate, it >>> works. Is this a bug? >> >> >> Could you provide the exact file and command line that you used to >> obtain this result? The second assert should not be provable (unless >> the call to test7 is guaranteed to never return successfully, in which >> case the code below the call is dead and any assertion on it holds) as >> long as there is no assigns for test7. In fact, Frama-C should have >> emitted a warning on a missing assigns clause. The kernel generates a >> clause based on the prototype of test7, which is absolutely not >> guaranteed to be sound and must at least be carefully reviewed. In the >> case at hand, as test7 takes a pointer as argument, Frama-C assumes >> that *x may be assigned by test7. Hence, no hypothesis on the content >> of *x after the call can be made. >> >> Best regards, >> -- >> E tutto per oggi, a la prossima volta >> Virgile >> _______________________________________________ >> Frama-c-discuss mailing list >> Frama-c-discuss at lists.gforge.inria.fr >> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss You should indicate that x and (all the cells of) a are separated as a precondition of test: requires \separated(x, a + (0..7)); Otherwise, if say x == &a[5], test2 could very well overwrite its value according to the assigns that you have written. I'd have expected the +ref model to succeed, which is the case if you only assigns *a (i.e. the first cell of a) in test2. Apparently the hypotheses made by the model do not ensure that x and a have completely separated bases, only different offsets. Best regards, -- E tutto per oggi, a la prossima volta Virgile