| 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 | |
| Platform | | OS | | OS Version | |
| 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 [Show Content] [Hide Content]
//@ 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;
}
|
|
Relationships 
Relationships