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] 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