--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on April 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C : Value Analysis : SWITCH vs IF



Hello Virgile,

Thanks a lot.

> int main () {
> float x;
> x = Frama_C_float_interval(-10.0,10.0);
> // this assertion is unknown
> //@ assert -5.0 <= x <= 5.0; x = x + 5.0; x = x + 5.0; // 
> this assertion is valid modulo the verification of the first 
> one //@ assert x >= 0.0; return 0; }
> 

Due to previous tests (say ... few years ago!), my *real* code embedded
something like x = myNonDet() ? -10.0 : 10.0; instead of
Frama_C_float_interval (myNonDet has no implementation, and the whole
code is analyzed with -lib-entry).

What relieved is that ranges of values for x were the same in both
cases: [-10. .. 10.] !!

But the Value Analysis does not behave in the same manner: with
"myNonDet()...", 1st assert is evaluated as NOT valid and then all the
code above is discarded. I'll try and investigate why later on!!!

Cheers,
Dillon

(last point: of course, state can be reduced by assertions ... what's
the hell made me writing the opposite!!!)