| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001076 | Frama-C | Plug-in > Eva | public | 2012-01-30 12:15 | 2012-09-19 17:16 | ||||
| Reporter | Jochen | ||||||||
| Assigned To | pascal | ||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Nitrogen-20111001 | ||||||||
| Target Version | Fixed in Version | Frama-C Oxygen-20120901 | |||||||
| Summary | 0001076: "volatile" ignored | ||||||||
| Description | Running "frama-c -val exm22.c" on the attached program produces the output "a in {0}". Running the same command after deleting the initialization of "a" in line 2 reports a run-time error (uninitialized variable access) in line 3. Both would be ok if "a" wasn't declared "volatile". In contrast to the 1st analysis result, the value-analysis manual says on p.43: "the analyzer does not assume that the value read from a volatile variable is identical to the last value written there." | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
pascal (reporter) 2012-01-30 23:38 |
Volatile variables are officially broken since around last July when a reorganization of the representation of programs was made and there was no industrial user to pay for the treatment of volatiles in the value analysis to be re-established. http://blog.frama-c.com/index.php?post/2011/07/21/Back-to-the-drawing-board Until someone steps up and funds the week or so of development and validation to fix this, you can assume that volatile variables in the value analysis do not work. |
|
Jochen (reporter) 2012-01-31 10:22 |
That's ok for me. You should sometimes update the according section (p.43) in the value-analysis manual. |
|
yakobowski (manager) 2012-06-10 18:26 |
This bug has been fixed at some point after Nitrogen. Notice that 'a' was actually considered volatile when computing expressions; only the printing of its final value was incorrect. volatile int a=0; return a+1; a ? {0} __retres ? [--..--] Notice that the code below is still considered incorrect. This is a conscious design choice. volatile int a; return a+1; |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2012-01-30 12:15 | Jochen | New Issue | |
| 2012-01-30 12:15 | Jochen | Status | new => assigned |
| 2012-01-30 12:15 | Jochen | Assigned To | => pascal |
| 2012-01-30 12:15 | Jochen | File Added: exm22.c | |
| 2012-01-30 23:38 | pascal | Note Added: 0002646 | |
| 2012-01-31 10:22 | Jochen | Note Added: 0002647 | |
| 2012-06-10 18:26 | yakobowski | Note Added: 0003095 | |
| 2012-06-10 18:26 | yakobowski | Status | assigned => resolved |
| 2012-06-10 18:26 | yakobowski | Resolution | open => fixed |
| 2012-09-19 17:15 | signoles | Fixed in Version | => Frama-C Oxygen-20120901 |
| 2012-09-19 17:16 | signoles | Status | resolved => closed |
| 2018-01-12 14:26 | signoles | Category | Plug-in > value analysis => Plug-in > Eva |
| Issue History |