WP doesn't warn about volatile variables
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; }