Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001372Frama-CPlug-in > Evapublic2013-02-20 09:232013-04-19 11:05
ReporterAnne 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001372: Extern function vs extern variable to get a random value
DescriptionI 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 InformationWith 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).
TagsNo tags attached.
Attached Filesc file icon toto.c [^] (606 bytes) 2013-02-20 09:23 [Show Content]

- Relationships

-  Notes
(0003703)
Anne (reporter)
2013-02-21 08:06

Sorry for the duplication, but #1164 seems to be private.
(0003704)
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.
(0003719)
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.

- Issue History
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-20 22:37 yakobowski Relationship added duplicate of 0001164
2013-02-21 08:06 Anne Note Added: 0003703
2013-02-21 09:51 yakobowski Note Added: 0003704
2013-02-21 17:43 Anne Note Added: 0003705
2013-02-21 18:58 signoles Note Added: 0003706
2013-02-22 07:59 Anne Note Added: 0003707
2013-02-27 23:50 yakobowski Note Deleted: 0003705
2013-02-27 23:50 yakobowski Note Deleted: 0003706
2013-02-27 23:50 yakobowski Note Deleted: 0003707
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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker