--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on April 2012 ---
On Sat, Apr 7, 2012 at 8:40 PM, Boris Yakobowski <boris at yakobowski.org> wrote: > Hi, > > I'm afraid you've both lost me a little there. > > On Sat, Apr 7, 2012 at 7:06 PM, Pascal Cuoq <pascal.cuoq at gmail.com> wrote: >> I think that the issue is that the GUI evaluates ACSL expressions. >> ACSL, unlike C, is total: *p == *p is true regardless of the validity >> of p and of the initializedness of *p. because it is an instance >> of an axiom. >> When you pass arr[i] in the GUI, you shouldn't get just arr[0], >> because "arr[i] == 0", for instance, is a valid ACSL assertion, >> and one that shouldn't get the status "true". >> Instead, the value analysis should say that it can't tell the value >> of arr[0]. > > I think you meant arr[i] Right, replace that last arr[0] by arr[i]. > the GUI does _not_ > evaluate ACSL expressions. While the contents of the "Evaluate > expression" are parsed as ACSL, they are converted back to C, and > evaluated as C. This means that computations overflow Precisely not. I do not feel strongly about this, but currently the "Evaluate expression" can be considered specified as manipulating ACSL for the following reasons: - The dialog window says "Enter an ACSL expression to evaluate". - If program variable x of type int is in [MIN_INT .. -1] in some point and you evaluate -x in the GUI at that point, you get [1..MAX_INT+1]. Pascal