0001372: Extern function vs extern variable to get a random value

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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

toto.c (606 bytes) 2013-02-20 09:23

//@ terminates \false; assigns \nothing; ensures \false;
void Frama_C_abort(void) __attribute__ ((noreturn));

//@ assigns \result \from \nothing;
extern double rand_double ();

//@ assigns \result \from \nothing; ensures \result <= 100;
extern double rand_double_post ();

extern double ext_double;

extern double rand_double_var () { return ext_double; }

double main (void) {
#if (T==1)
  double v = ext_double;
#elif (T==2)
  double v = rand_double ();
#elif (T==3)
  double v = rand_double_post ();
#elif (T==4)
  double v = rand_double_var ();
#endif
  if (v > 100) Frama_C_abort ();
  return v;
}

toto.c (606 bytes) 2013-02-20 09:23

Relationships

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.

Notes

Date Modified	Username	Field	Change
Issue History
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

Issue History