--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on April 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Unsound results from the value plugin on some arrays access



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