Anonymous Login Frama-C issues should now be submitted on Frama-C's GitLab
2021-03-06 03:08 CET
  

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 
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 Files
  • c file icon main.c (360 bytes) 2017-02-03 12:11 - 
    #define _FBS(x) int _FBS = (x);

#define BWRP_WRPROTECT_OFF   0xFFFF
#define BSS_NO_FLASH         0xFFFF
#define BSS_NO_BOOT_CODE     0xFFFF
#define RBS_NO_RAM           0xFFFF
#define RBS_NO_BOOT_RAM      0xFFFF

_FBS( BWRP_WRPROTECT_OFF & BSS_NO_FLASH & BSS_NO_BOOT_CODE & RBS_NO_RAM & RBS_NO_BOOT_RAM );

void main(void)
{
    char x = 128;
}
    c file icon main.c (360 bytes) 2017-02-03 12:11 +

-Relationships
+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.
+Notes

-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
+Issue History