--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on August 2017 ---
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?