Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Frama-C : Value Analysis : SWITCH vs IF
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
  • Date: Thu, 9 Apr 2009 10:00:22 +0200
  • In-reply-to: <20090408181558.3ef6c548@is005115>
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!!!)