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

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