Frama-C Bug Tracking System - Frama-C
View Issue Details
0001372Frama-CPlug-in > Evapublic2013-02-20 09:232013-04-19 11:05
Anne 
yakobowski 
normalminorhave not tried
closedfixed 
Frama-C Oxygen-20120901 
Frama-C Fluorine-20130401 
0001372: Extern function vs extern variable to get a random value
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...
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).
No tags attached.
c toto.c (606) 2013-02-20 09:23
https://bts.frama-c.com/file_download.php?file_id=474&type=bug
Issue History
2013-02-20 09:23AnneNew Issue
2013-02-20 09:23AnneStatusnew => assigned
2013-02-20 09:23AnneAssigned To => yakobowski
2013-02-20 09:23AnneFile Added: toto.c
2013-02-20 22:37yakobowskiRelationship addedduplicate of 0001164
2013-02-21 08:06AnneNote Added: 0003703
2013-02-21 09:51yakobowskiNote Added: 0003704
2013-02-21 17:43AnneNote Added: 0003705
2013-02-21 18:58signolesNote Added: 0003706
2013-02-22 07:59AnneNote Added: 0003707
2013-02-27 23:50yakobowskiNote Deleted: 0003705
2013-02-27 23:50yakobowskiNote Deleted: 0003706
2013-02-27 23:50yakobowskiNote Deleted: 0003707
2013-02-28 00:00yakobowskiNote Added: 0003719
2013-02-28 00:00yakobowskiStatusassigned => resolved
2013-02-28 00:00yakobowskiResolutionopen => fixed
2013-04-19 11:05signolesFixed in Version => Frama-C Fluorine
2013-04-19 11:05signolesStatusresolved => closed
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0003703)
Anne   
2013-02-21 08:06   
Sorry for the duplication, but #1164 seems to be private.
(0003704)
yakobowski   
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.
(0003719)
yakobowski   
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.