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



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?

On Thu, Aug 3, 2017 at 1:49 PM, Yifan Lu <me at yifanlu.com> wrote:
> I have some global const pointers that are unique and never change.
> However, whenever I add one to an assigns clause, it seems that any
> assumptions about other pointer values goes out the window. So I tried
> to add:
>
> -wp-unalias-vars globalx,globaly
>
> but this assertion still fails
>
> extern int * const globalx;
> extern int * const globaly;
>
> int main(int argc, const char *argv[]) {
>   //@ assert globalx != globaly;
>   return 0;
> }
>
> How can I ensure that these global variables are non-changing?