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,

I'm afraid you've both lost me a little there.

On Sat, Apr 7, 2012 at 7:06 PM, Pascal Cuoq <pascal.cuoq at gmail.com> wrote:
> I think that the issue is that the GUI evaluates ACSL expressions.
> ACSL, unlike C, is total: *p == *p is true regardless of the validity
> of p and of the initializedness of *p. because it is an instance
> of an axiom.
> When you pass arr[i] in the GUI, you shouldn't get just arr[0],
> because "arr[i] == 0", for instance, is a valid ACSL assertion,
> and one that shouldn't get the status "true".
> Instead, the value analysis should say that it can't tell the value
> of arr[0].

I think you meant arr[i], or arr[72]? In any case, the GUI does _not_
evaluate ACSL expressions. While the contents of the "Evaluate
expression" are parsed as ACSL, they are converted back to C, and
evaluated as C. This means that computations overflow, arrays are
finite, etc.

(Disclaimer: this is not perfect ; the types in the expression may not
be the ones the user wants ; thus overflow may be treated in
unexpected ways.)

> In the value analysis proper, there is a filtering step before calling
> Cvalue.Model.find
> to keep only the valid locations in the argument location (and
> emit the appropriate alarm if the location is not entirely valid).
> I guess you could say that the API for calling Cvalue.Model.find
> is that it should only be applied to arguments that have been
> filtered thus. But since Cvalue.Model.find has a ~with_alarms
> argument already, we could make it emit alarms
> when it notices that the location passed is not completely valid.
> That would be less surprising for plug-in authors who call
> Cvalue.Model.find directly.

I'm sorry, but I'm reasonably sure that Cvalue.Model.find already does
exactly that, that being "check validity, and emit an alarm. In fact,
due to the existence of bases with Unknown validity, no other solution
would be safe.

I have written some code to test this hypothesis, attached to this
mail. I read the contents of *x on the return statement in two
different ways, and in both cases I get an alarm. Writing the code
slightly differently shows that the alarm is the correct one, ie
\valid(x) (on Nitrogen).

On Fri, Apr 6, 2012 at 2:37 PM, Pierre Karpman
<Pierre.Karpman at rennes.supelec.fr> wrote:
> 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?

Again, this is strange. As shown by the code I attached, an alarm
ought to be raised. Can you pretty-print the location you're giving as
argument to Cvalue.Model.find (on your original code or mine)? Thanks.

-- 
Boris
-------------- next part --------------
A non-text attachment was scrubbed...
Name: pk.c
Type: text/x-csrc
Size: 200 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120407/1ea54f75/attachment.c>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: pk.ml
Type: application/octet-stream
Size: 1530 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120407/1ea54f75/attachment.obj>