| Anonymous | Login | Signup for a new account | 2019-06-15 23:40 CEST |  |
| Main | My View | View Issues | Change Log | Roadmap | Repositories |
| 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 | ||||||
| Platform | OS | OS Version | |||||||
| 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 |  exm22.c [^] (85 bytes) 2012-01-30 12:15 [Show Content]
| ||||||||
 Relationships |
|
 Relationships |
|
Notes |
|
|
(0002646) 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. |
|
(0002647) 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. |
|
(0003095) 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 |
| Copyright © 2000 - 2019 MantisBT Team |
|