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: Wed, 8 Apr 2009 17:18:08 +0200
  • In-reply-to: <20090408160715.7363d7d7@is005115>
Hello Virgile,

Thanks for your answer.

Clearly, the problem is that one may need to reduce the current computed
state (which is currently forbidden ... I know!), the range of values.

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.



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.

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
Value Analysis? 
... and at first ... is this feasible?

Thanks in advance for any comments!
Best regards,
Dillon