Pip Cet wrote:
eassume (global == 0); eassume (f ()); #else eassume (global == 0 && f ()); ... extern int global;int f(void) { return ++global; }
This is not a valid use of 'assume'. It's documented that assume's argument should be free of side effects.
It would be nice if 'assume (R)' reported an error if R has side effects, and generated a warning unless the compiler can verify that R is free of side effects. However, these niceties would require better support from the compiler.
If you want your program to behave predictably, in the strict sense, you cannot ever use the current assume() API.
I'm not sure what you mean by "in the strict sense". It's true that programs can misuse 'assume' and get undefined behavior, but that's kind of the point....
