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] precision for expression evaluation in a condition

  • Subject: [Frama-c-discuss] precision for expression evaluation in a condition
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Tue, 15 Mar 2011 21:17:55 +0100
  • In-reply-to: <AANLkTink3Q_fvtMV55j1sOosg4VO8=337kvMCAurOW0k@mail.gmail.com>
  • References: <AANLkTink3Q_fvtMV55j1sOosg4VO8=337kvMCAurOW0k@mail.gmail.com>
On Tue, Mar 15, 2011 at 6:36 PM, xavier kauffmann wrote:
> when evaluating bar at the toto = 1; line I get:
> Before statement:
> bar ? {1234; }
> At next statement:
> bar ? [--..--]
> [...]
> Even if there is only one line in the else branch?
> If possible I'm looking for a way to evaluate an expression at the
> statement, not before or after.
> If the statement modifies the expression it does not work but if it is not
> related to it, shouldn't the value analysis be able to provide a value or
> range for this expression?

With Frama-C's representation of the AST, there is really no place you
might want to observe the values of variables other than before a
statement or after a statement. This said, note that your version does
not claim it gives you the values of bar after the statement. It says
it gives you the value "at next statement" (which should in some cases
be "at next statements").

After this introduction, please read
http://blog.frama-c.com/index.php?post/2011/01/11/Seven-errors-game
and note that it was published before the release of Frama-C Carbon
20110201.

Regarding the "if it is not related to it, shouldn't the value
analysis be able to provide a value or range for this expression?"
part of your question: of course, it can provide the value of an
unrelated expression. If your program has a thousand globals, the
value of each global at each statement is saved just in case you later
want to inspect the value of that variable at that program point.

> when I was hoping for something like
> bar ? [--..--] - {1234}
> based on the evaluation of bar at the toto = 1 and toto = 3 lines
> Is there a way to get these exclusions from the value analysis?

Well, you may have noticed that "[--..--] - {1234}" is not in the
documented list of formats in which the value analysis can display
sets of values. However, you may get the sets [-2^31 .. 1233] and
[1235 .. 2^31-1] programmatically, provided you are willing to insert
an annotation to guide the value analysis.

Considering the lab's current focus on the verification of syntactic
coding rules, if I were you, I wouldn't hold too much hope of seeing
1/ how to access these sets documented;
2/ their computation made entirely automatic (without need for a user
annotation).

Pascal