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] multiple switch on one variable

Hello,

your example brings up several remarks.

> /*@ ensures \result == x || \result == a + b; */
>
> int main (int a, int b, int x)

1/ You are writing a post-condition involving arguments
that are modified inside the function as if they were
local variables. The occurrences of a and b in the
post-condition refer to the initial values of a and b, not
the values at the end of the function. Are you sure
you want to do this? I am sure I will get confused before
the end of this discussion.

2/ In Frama-C Carbon with alt-ergo 0.92.1, the post-condition
goals for your function are all proved. There are some arithmetic
overflow warnings, but considering that you do not give the
provers hypotheses on the values of variables that could prevent
overflows, I would tend to think it is right without looking.

3/ It is principally about the value analysis and in fact,
option -jessie may even automatically imply -simplify-cfg
(I do not know how it works), but you may be interested in
this blog post:

http://blog.frama-c.com/index.php?post/2011/02/28/switch-statements-in-the-value-analysis

Pascal