--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on June 2011 ---
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