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,

<flamewar suit="on">

Before this escalates further on, I will try to answer a few points:

1) as numerous others have pointed out, Value's domains are
non-relational. Thus, _in genera_l they cannot be used to prove the
kind of equality assertions you have written. This is a conscious
design choice, as the WP can be used instead.

However, there are good reasons to position an "Unknown" status on
such assertion. First, in some cases, Value could return Valid or
Invalid statuses. This would be the case if both val and retval
contained singleton values, or non-overlapping sets. Second, "Unknown"
marks the fact that Value actually read (and tried to prove) the
assertion. Typically, we position no statuses on "assigns" clauses for
functions with definitions, because we do not read them. In your
example, if you are courageous enough to write a 256 cases
disjunction, your assertions will all get proven.

For more complicated assertions, typically those with user-defined
predicates, 'Unknown' means "the assertion was not understood". We are
currently considering changing this to position no status in this
case. However, things get a bit muddy with disjunctions "simple
assertion || very complicated assertion".

2) writing relational domains with modulo arithmetics is not as
trivial as it seems, because one must be wary of overflows. The fact
that ACSL uses unbounded arithmetics complicates things further.

3) as Boris Hollas pointed out, an 'Unknown' status does not
intrinsically indicate a deficiency in the analyzer. Most properties
are in general undecidable, so no analyzer can hope to position
precise statuses all the time.

4) regarding your initial question about behaviors. Currently, the
value analysis evaluates all the behaviors it deems possible
('active') at a possible call simultaneously. In your case, both your
negative and positive behaviors are possible, given the range of val.
The message "but it is unknown if the behavior is active" warns you
that a status is positioned on the postcondition of the behavior, but
this behavior could in fact be inactive on real executions. If you
want to avoid those warnings, position your disjunction _before_ your
call:

	/*@ assert ( in_int8 < 0 ) || ( in_int8 >= 0 ); */
	uint8 out_uint8 = abs8(in_int8);

Hope this helps,

-- 
Boris