--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on August 2017 ---
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