--- layout: fc_discuss_archives title: Message 14 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 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