Anonymous | Login | Signup for a new account | 2019-02-17 03:55 CET | ![]() |
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 | ||||
0002277 | Frama-C | Plug-in > Eva | public | 2017-02-03 12:11 | 2017-05-31 19:05 | ||||
Reporter | Max P. | ||||||||
Assigned To | yakobowski | ||||||||
Priority | normal | Severity | major | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Platform | OS | OS Version | |||||||
Product Version | Frama-C 14-Silicon | ||||||||
Target Version | Fixed in Version | Frama-C 15-Phosphorus | |||||||
Summary | 0002277: Operability depends on the order of options changes | ||||||||
Description | If value analysis is run on attached file with default options Frama-C makes no warnings. If you then turn on -warn-signed-downcast and repeat the analysis, a warning appears on the Message tab: main.c:13:[value] warning: signed downcast. assert 128 ≤ 127; If you reload Frama-C and turn on -warn-signed-downcast before first running of analysis, analysis will not run. On Console tab will be output: [value] Initial state computed [value:initial-state] Values of globals at initialization NOT ACCESSIBLE [value] Value analysis not started because globals initialization is not computable. If you then turn off -warn-signed-downcast and repeat the analysis, nothing changes. | ||||||||
Steps To Reproduce | 1. Run Frama-C GUI. 2. Add attached file. 3. Turn on -warn-signed-downcast option. 4. Run value analysis. 5. Turn off -warn-signed-downcast option. 6. Run value analysis. 7. Reload Frama-C GUI. 8. Add attached file. 9. Run value analysis. 10. Turn on -warn-signed-downcast option. 11. Run value analysis. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files | ![]() | ||||||||
![]() |
|
(0006361) signoles (manager) 2017-02-24 15:45 |
I am not able to reproduce your issue. Could you please set the option -journal-enable when running the GUI and attached the generated file .frama-c/frama_c_journal.ml: $ frama-c-gui -journal-enable $ ls .frama-c frama_c_journal.ml |
(0006365) Max P. (reporter) 2017-03-01 14:38 |
Try to use -machdep x86_16. |
(0006369) signoles (manager) 2017-03-02 16:26 |
Indeed it is weird. Boris, here is how to reproduce the issue without the GUI (same output with the dev version). // run 1 $ frama-c -machdep x86_16 main.c -val -then -warn-signed-downcast // run without checking signed downcast [value] Analyzing a complete application starting at main <...> // run checking signed downcast [value] Analyzing a complete application starting at main <...> main.c:13:[value] warning: signed downcast. assert 128 ≤ 127; <...> // run 2 which directly checks signed downcast without any previous run $ frama-c -machdep x86_16 main.c -val -warn-signed-downcast <...> [value] Computing initial state main.c:9:[value] warning: signed downcast. assert ((unsigned int)((unsigned int)((unsigned int)(0xFFFF & 0xFFFF) & 0xFFFF) & 0xFFFF) & 0xFFFF) ≤ 32767; main.c:9:[value] Evaluation of initializer '(int)((((0xFFFF & 0xFFFF) & 0xFFFF) & 0xFFFF) & 0xFFFF)' failed |
(0006377) yakobowski (manager) 2017-03-08 00:37 |
Interesting, there is indeed a bug here. The computation of the initial state should depend on analysis parameters such as -warn-signed-downcast (because the initial state may fail to be computed, as demonstrated here), but for some reasons this is not captured. I will investigate. |
(0006379) yakobowski (manager) 2017-03-08 12:34 |
Will be fixed in Phosphorus. |
![]() |
|||
Date Modified | Username | Field | Change |
2017-02-03 12:11 | Max P. | New Issue | |
2017-02-03 12:11 | Max P. | File Added: main.c | |
2017-02-24 15:41 | signoles | Assigned To | => signoles |
2017-02-24 15:41 | signoles | Status | new => assigned |
2017-02-24 15:45 | signoles | Note Added: 0006361 | |
2017-02-24 15:45 | signoles | Status | assigned => feedback |
2017-03-01 14:38 | Max P. | Note Added: 0006365 | |
2017-03-01 14:38 | Max P. | Status | feedback => assigned |
2017-03-02 16:26 | signoles | Note Added: 0006369 | |
2017-03-02 16:26 | signoles | Assigned To | signoles => yakobowski |
2017-03-02 16:28 | signoles | Category | Kernel => Plug-in > value analysis |
2017-03-08 00:37 | yakobowski | Note Added: 0006377 | |
2017-03-08 12:34 | yakobowski | Note Added: 0006379 | |
2017-03-08 12:34 | yakobowski | Status | assigned => resolved |
2017-03-08 12:34 | yakobowski | Resolution | open => fixed |
2017-03-08 12:34 | yakobowski | Fixed in Version | => Frama-C 15-Phosphorus |
2017-05-31 19:04 | signoles | Fixed in Version | Frama-C 15-Phosphorus => |
2017-05-31 19:04 | signoles | Fixed in Version | => Frama-C 15-Phosphorus |
2017-05-31 19:05 | signoles | Status | resolved => closed |
2018-01-12 14:26 | signoles | Category | Plug-in > value analysis => Plug-in > Eva |
Copyright © 2000 - 2019 MantisBT Team |