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



Hi again,

On Fri, Apr 6, 2012 at 11:24 AM, Pierre Karpman
<Pierre.Karpman at rennes.supelec.fr> wrote:
> although arr[i] is not used at mark1, I'd still like to know what the value
> analysis can say about it. This can be done e.g. in the GUI by asking to
> evaluate the expression "arr[i]" at this statement, which will give me the
> result "arr[i] == 0"; this is confusing because the right way to interpret
> the result would be "if this expression were to be in the source; if the
> program didn't fail, then it would have this value", but there isn't any
> hint about which conditions are necessary for the program not to
> pretend-fail when we pretend-evaluate it, as there would be in the form of
> an assert statement if the expression was actually in the source.
> I will probably add the checks I need in my code, then.

The GUI is indeed missing a warning telling that the requested
expression may not evaluate in all cases. We will probably add this
for the next release.

For your plugin, you can also do a few things. As you have probably
noticed, the function that evaluates expressions take a ~with_alarms
parameter as argument. This argument is supposed to indicate what
happens when a possible error is detected. One possibility is
<nothing>, which corresponds to CilE.warn_none_mode. An another
possibility is to use the CilE.Acall constructor, with a function that
prints your own warning, or set a reference meaning "an alarm has
occurred". In both cases (and unless your user-defined function raises
an exception), the functions will return what happens when evaluation
is defined.

Hope this helps,

-- 
Boris