Operability depends on the order of options changes
ID0002277: This issue was created automatically from Mantis Issue 2277. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002277 | Frama-C | Plug-in > Eva | public | 2017-02-03 | 2017-05-31 |
| Reporter | Max P. | Assigned To | yakobowski | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C 14-Silicon | Target Version | - | Fixed in Version | Frama-C 15-Phosphorus |
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 :
- Run Frama-C GUI.
- Add attached file.
- Turn on -warn-signed-downcast option.
- Run value analysis.
- Turn off -warn-signed-downcast option.
- Run value analysis.
- Reload Frama-C GUI.
- Add attached file.
- Run value analysis.
- Turn on -warn-signed-downcast option.
- Run value analysis.