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,
> Hi again,
>
> On Fri, Apr 6, 2012 at 11:24 AM, Pierre Karpman
> <Pierre.Karpman at rennes.supelec.fr  <http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss>>  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.

Yes, I guess it'd be a bit less ambiguous :)

>
> 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.
The only function I'm calling that uses alarms is Cvalue.Model.find, and 
I already registered an abort function to avoid using inconsistent 
results. This does help in some cases (like filtering out variables that 
are not always defined) but not in this one.
Is this ("find") the function you were thinking about?

Cheers,
Pierre
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120406/3572a615/attachment.html>