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 mer 08 avr 2009 17:18:08 CEST,
"Pariente Dillon" <Dillon.Pariente at dassault-aviation.com> a ?crit :

> Suppose that at a certain control point, we have:
> 
> x = f(a); // Suppose Value Analysis obtained from f() that x's values
> are in [-10.0 .. 10.0]
> 
> ...
> 
> //@ assert -5.0<=x<=5.0;
> 	// Suppose we know that f()'s results are over-approximated by
> Value Analysis
> 	// and that the assert above is validated by Jessie (or it is up
> to the user to justify it).
> 	// The point is: Value Analysis considers this assert as Not
> valid and discards all of the statements below.

I'm not sure I'm following you: the value analysis will consider the
assert as Unknown, and the analysis will continue, with x being in the
interval [-5.0; +5.0], as can be seen in the following example

/* compile-command: frama-c -val `frama-c -print-path`/builtin.c test.c
*/

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;
}

> It will be of high interest for end-users to be able to express such
> range's reducing to the Value Analysis: in order to allow Value Analysis
> to propagate this new range.
> 

This is already the case. The issue is that currently the value
analysis does only handle closed intervals (i.e. something like
x_l<=x<=x_h). So if your assertion is of the form x_l < x < x_h, it
will use a slightly larger interval x_l<=x<=x_h[1]

> So the question is: will it be possible, in the (mid or long term?)
> future, to propagate user's assertions as relations between variables in

In general, no: there is no abstract domain that can represent
precisely an arbitrary user assertion. For particular assertions, which
fit well with the underlying domain, this is feasible (but of course,
the more complex the assertion is, the more precise and thus costly the
abstract domain must be). In particular, the domains of the APRON
library (http://apron.cri.ensmp.fr/library/) might get incorporated at
some point.

Best regards,
-- 
Virgile Prevosto
Ing?nieur-Chercheur, CEA, LIST
Laboratoire de S?ret? des Logiciels
+33/0 1 69 08 71 83
[1] This is not an issue with integers, as x_l < x is equivalent to 
x_l + 1 <= x, but this equivalence does not hold for reals.