--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on April 2009 ---
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!!!)