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: Tue, 14 Apr 2009 17:38:06 +0200
  • In-reply-to: <20090409105924.1ad72c3f@is005115>
Hello,

Please, to sum up the situation, confirm a few remarks about non-deterministic functions and validation of user's annotation.

In the following example (*x and *min are inputs, *y is the output equal to the clipping of *x wrt *min):

void g (float * min,float * x,float * y)
{ 
*x = Frama_C_float_interval(-1000.0,1000.0);
*min = Frama_C_float_interval(-100.0,100.0);
if(*x >= *min) *y = *x; else *y = *min;
//@ assert *y >= *min;
}

the assert status computed by Value Analysis is "Unknown".
Replacing "*min = Frama_C_float_interval(-100.0,100.0);" 
with "*min = nd() ? -100.0 : 100.0;" (-slevel > 2)
allows to validate the assert (i.e., replacing the whole interval with an "enumerate" of states yields a "Valid" status).
Is it because Value Analysis is able to distinguish the 4 (?) different cases (the case in which *min==-100 with *x lower than or greater to *min ; and the case in which *min==100 ...)? And such distinction can not be done when *min is an interval?

With the code above (only using Frama_C_float_interval), Value Analysis will not consider "*y >= *min" as Valid at the return control point, even if it is located after the aforementionned assert.
This is due to the fact that one can reduce the state with intervals of values, but not with relations between variables, as Virgile mentionned in one of his previous mails (that is to say, not before embedding APRON library or equivalent), isn't it?

Then, with the current version of the tool, do you see any means to make Value Analysis take into account the assert in calling functions to g()?

Thanks in advance for your answers!
Best regards,
Dillon
 

> -----Message d'origine-----
> De : frama-c-discuss-bounces at lists.gforge.inria.fr 
> [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] De la 
> part de Virgile Prevosto
> Envoy? : jeudi 9 avril 2009 10:59
> ? : frama-c-discuss at lists.gforge.inria.fr
> Objet : Re: [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.