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] [Value analysis] Validating a function with behavior spec.

Hi Sylvain,

On Mon, Apr 16, 2012 at 10:34 AM, sylvain nahas
<sylvain.nahas at googlemail.com> wrote:
>> If you want to avoid those warnings, position your disjunction _before_ your
>> ? ? ? ?/*@ assert ( in_int8 < 0 ) || ( in_int8 >= 0 ); */
>> ? ? ? ?uint8 out_uint8 = abs8(in_int8);
>
> So a "requires" in a contract hasn't the same effect?

Good remark. I focused on the assertion at the beginning of abs8, and
forgot about your precondition. The answer is two-fold. Disjunction in
'requires' are used to propagate states separately, provided there is
enough slevel at the beginning of the function to split the
disjunction (it is the case here). You can check that by adding a
Frama_C_show_each(val) just before your assert: you will get two
different lines in the log.

However, the body of the function is not analyzed N times, just 1 time
with N different states. There are subtle differences between these
two possibilities, including which behaviors are active. Here
positive_or_zero is active only in the case "val >= 0', and
conversely, but we cannot easily keep track of this information. By
adding a disjunction before the call, things are different: the
function is analyzed twice.

>From a general standpoint, Value has a certain latitude on what to do
on behaviors and preconditions, as many approaches are correct
(sound), but not equivalent in terms of precision and computation
time. In your example, the 'requires' is useful, but should not be
given the 'assumes', 'disjoint' and 'complete' clauses, since those
contain all the needed information. For Oxygen, I would like to
implement alternative strategies such as automatic split, at least for
complete and disjoint behaviors.

HTH,

-- 
Boris