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