0002277: Operability depends on the order of options changes

(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

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.

Relationships