--- layout: fc_discuss_archives title: Message 7 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?



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