Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002277Frama-CPlug-in > Evapublic2017-02-03 12:112017-05-31 19:05
ReporterMax P. 
Assigned Toyakobowski 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C 14 Silicon 
Target VersionFixed in VersionFrama-C 15 Phosphorus 
Summary0002277: Operability depends on the order of options changes
DescriptionIf 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 Reproduce1. 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.
TagsNo tags attached.
Attached Filesc file icon main.c [^] (360 bytes) 2017-02-03 12:11 [Show Content]

- Relationships

-  Notes
(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.

- Issue History
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 - 2018 MantisBT Team
Powered by Mantis Bugtracker