Extern function vs extern variable to get a random value

ID0001372: This issue was created automatically from Mantis Issue 1372. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0001372	Frama-C	Plug-in > Eva	public	2013-02-20	2013-04-19

Reporter	Anne	Assigned To	yakobowski	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	have not tried
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Oxygen-20120901	Target Version	-	Fixed in Version	Frama-C Fluorine-20130401

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).

## Attachments
- [toto.c](/uploads/9e28b543bd0896a04a18d16dd7ead4cf/toto.c)