Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Proper usage of -wp-unalias-vars?

  • Subject: [Frama-c-discuss] Proper usage of -wp-unalias-vars?
  • From: me at yifanlu.com (Yifan Lu)
  • Date: Thu, 3 Aug 2017 13:49:58 -0700
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?