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

>> 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.

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].

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.

In fact, you could call it a bug that Cvalue.Model.find does not
already do that, but this cannot be observed from
the commandline version of Frama-C (to the best of my knowledge)
for the aforementioned reason that out of bounds accesses are
handled in a preliminary step when it's the value analysis
calling Cvalue.Model.find.
I am reluctant to use the B-word for usages that have not
been defined as the commandline usage has in the value
analysis manual and in the blog.

Pascal