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 9:03 PM, Pascal Cuoq <pascal.cuoq at gmail.com> wrote:
> 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".

It says so because we currently do not have any facility for parsing a
string into a C expr/lval etc. Thus, the ACSL parsers are used
instead. But any ACSL expression which cannot be translated back into
a C one is refused -- even one which Value would correctly evaluate in
an assertion or a requires.

Both an "evaluate as C" and "evaluate as ACSL" option would be useful.
However, both require a very non-trivial amount of work, and no one
has had the courage to tackle the issue. Patches, preferably not ones
that add a blinking disclaimer, are welcome.

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

My disclaimer in the previous message was there for a reason. No real
attempt to give values the "good" type is done, so most integer
expressions get type long long. If you declare your variable x
directly with this type, computations on it will overflow.
Alternatively, you can multiply your original x by itself enough
times.

-- 
Boris