--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on August 2017 ---
Thank you! That worked. On Fri, Aug 4, 2017 at 9:54 AM, Virgile Prevosto <virgile.prevosto at m4x.org> wrote: > 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 > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss