View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001372 | Frama-C | Plug-in > Eva | public | 2013-02-20 09:23 | 2013-04-19 11:05 | ||||
Reporter | Anne | ||||||||
Assigned To | yakobowski | ||||||||
Priority | normal | Severity | minor | Reproducibility | have not tried | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Oxygen-20120901 | ||||||||
Target Version | Fixed in Version | Frama-C Fluorine-20130401 | |||||||
Summary | 0001372: Extern function vs extern variable to get a random value | ||||||||
Description | I am trying to build an environment to represent the inputs of the application that I study with the value analysis. I tried different things : ~~~~~~~~~~~~~ 1/ double v = ext_double; assert (v <= 100); with the global variable : extern double ext_double; gives what I want: v ? [-1.79769313486e+308 .. 100.] ~~~~~~~~~~~~~ 2/ double v = rand_double (); assert (v <= 100); with: //@ assigns \result \from \nothing; extern double rand_double (); gives a warning that I don't understand: toto.c:25:[value] warning: converting value to float: assert(Ook) and doesn't use the assert (?): v ? [--..--] ~~~~~~~~~~~~~ 3/ double v = rand_double_post (); assert (v <= 100); with: //@ assigns \result \from \nothing; ensures \result <= 100; extern double rand_double_post (); gives the same warning twice: toto.c:21:[value] warning: converting value to float: assert(Ook) toto.c:25:[value] warning: converting value to float: assert(Ook) and doesn't work either: v ? [--..--] ~~~~~~~~~~~~~ 4/ double v = rand_double_var (); assert (v <= 100); with: extern double rand_double_var () { return ext_double; } gives no warning, and works as expected: v ? [-1.79769313486e+308 .. 100.] ~~~~~~~~~~~~~ Shouldn't the four initializations give the same results ? Sorry if it is about something that I didn't understand... | ||||||||
Additional Information | With the attached file, see previous results with the command: $ frama-c -val toto.c -cpp-extra-args="-DT=1" with different values of T (1 to 4). | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
Anne (reporter) 2013-02-21 08:06 |
Sorry for the duplication, but #1164 seems to be private. |
yakobowski (manager) 2013-02-21 09:51 |
No problem, I actually opened 1164. This issue is related to the handling of NaN/Infinities. Value no not propagate, and instead raises an alarm, but it can still encounter trough external functions or unsafe casts. |
yakobowski (manager) 2013-02-28 00:00 |
This bug will be fixed in Fluorine. - the mysterious messages "converting value to float: assert(Ook)" do not appear anymore - at the end of the analysis, v IN [-1.79769313486e+308 .. 100.] holds in all four cases. - for cases 2 and 3, there is an alarm on the first read of v at ligne 24. This takes into account the fact that rand_double/rand_double_post may return a NaN or an infinity. - it is currently not possible to use assertions to express that a NaN/Infty float is within a range. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2013-02-20 09:23 | Anne | New Issue | |
2013-02-20 09:23 | Anne | Status | new => assigned |
2013-02-20 09:23 | Anne | Assigned To | => yakobowski |
2013-02-20 09:23 | Anne | File Added: toto.c | |
2013-02-21 08:06 | Anne | Note Added: 0003703 | |
2013-02-21 09:51 | yakobowski | Note Added: 0003704 | |
2013-02-28 00:00 | yakobowski | Note Added: 0003719 | |
2013-02-28 00:00 | yakobowski | Status | assigned => resolved |
2013-02-28 00:00 | yakobowski | Resolution | open => fixed |
2013-04-19 11:05 | signoles | Fixed in Version | => Frama-C Fluorine |
2013-04-19 11:05 | signoles | Status | resolved => closed |
2018-01-12 14:26 | signoles | Category | Plug-in > value analysis => Plug-in > Eva |