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



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