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

Le jeu 09 avr 2009 10:00:22 CEST,
"Pariente Dillon" <Dillon.Pariente at dassault-aviation.com> a ?crit :

> 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!!!

Well, I suspect that you have a -slevel n (with n > 0) on your command
line: in this case, the two possible states (-10.0 and 10.0) are kept
separated, and thus the assertion in invalid. If you don't use that
option, then the two states are merged at the end of the assignment,
leaving you with the whole interval as an overapproximation of both (in
fact, this is the smallest interval that contains both -10 and 10), and
the assertion gets the expected unknown status. Of course, with
Frama_C_float_interval, you get directly the whole interval, so -slevel
does not change anything.

Best regards,
-- 
Virgile Prevosto
Ing?nieur-Chercheur, CEA, LIST
Laboratoire de S?ret? des Logiciels
+33/0 1 69 08 71 83