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



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?