--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on August 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Proper usage of -wp-unalias-vars?



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