GitLab

ID0001801: This issue was created automatically from Mantis Issue 1801. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0001801	Frama-C	Plug-in > wp	public	2014-06-06	2014-06-06

Reporter	Anne	Assigned To	correnson	Resolution	open
Priority	normal	Severity	major	Reproducibility	have not tried
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Neon-20140301	Target Version	-	Fixed in Version	-

Description :

I noticed that WP doesn't handle volatile variables, which is not a problem, but the problem is that it proves properties about them without any warning at all, which a quiet embarrassing I suppose.

Steps To Reproduce :

$ frama-c -wp-fct main test_volatile.c

volatile int v = 10; //@ ensures \result == 10; int main (void) { int x = v; //@ assert v == 10; v = 3; //@ assert v == 3; return x; }