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



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