SYSTEM WARNING: 'session_name(): Cannot change session name when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 231

SYSTEM WARNING: 'session_set_cookie_params(): Cannot change session cookie parameters when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 232

mantis:frama-c:issue:156 [Frama-C]

User Tools

  • Logged in as: anonymous (anonymous)
  • Log Out

Site Tools


mantis:frama-c:issue:156

This page details the semantics of ACSL \valid predicate related to Issue ~~Mantis:156~~ in the BTS.

\valid(a+x..y) and array arguments

Context

Consider the following function with its pre-condition:

/*@ require \valid(a+(low..high)); */
void f(int a[], int low, int high) {
  a[high] = 1;
}

With this single pre-condition, it is not possible to prove that the access to a[high] is correct, since we haven't said that low ⇐ high: If this is not the case, then low..high is the empty range, and thus the pre-condition amounts to \valid(\empty) which is always true (for this to hold, all the element(s) of the empty set must be valid pointers, or conversely, no element of the empty set must be invalid, which is trivially verified, since there's no element at all).

Questions

Shouldn't \valid(\empty) be considered false?

No, as said above, the fact that ''\valid(empty)'' is true is a consequence of the definition of ''\valid'' with an universal
quantification over the set given as argument: When the set is empty, the property always holds.

Shouldn't such a precondition triggers an implicit pre-condition that low <= high?

No ACSL formula adds implicit constraints on the program state. This is true here, but also for a statement
such as 
<code>
//@ assert *x == 0;
</code>
which does not implicitely require ''\valid(x)''. Of course, if you can not prove that x is a valid pointer,
you won't be able to prove that its content is equal to 0, but the formula itself
can be written and has a precise meaning. Whether it holds or not is another subject.

In our case, the pre-condition states that the function should behave correctly even in the case where low > high. This could for instance be done by guarding the pointer access with an if statement, or by having the developer convincing the designer to modify the specification. Again, this is a different issue from the pre-condition alone.

Shouldn't the fact that a is an array triggers an implicit pre-condition that 0<=low?

Most of the time, a parameter declared as an array is the same thing as a pointer, thus this does not add any information about the validity. There is only one exception in the C standard (section 6.7.5.3):

void f(int a[static 10], int low, int high);

in which case all calls to f must give as argument a pointer to the first element of an array of size at least 10.

But even in this case, we only have an additional information on a (namely \valid(a+0..9)). This does not tell anything about the value of low:

int A[2][10];
f(A[1]);

is a perfectly correct call, where \valid(a+(-10..9)) holds.

What about the respective truth value of \valid_range(a,low,high) and \valid(a+(low..high)) ?

The jessie library defines \valid_range in terms of \offset_min and \offset_max, the minimal (resp. maximal) offset that can be added to a pointer to obtain a valid pointer. Namely,

  \valid_range(a,low,high) <==> \offset_min(a) <= low && \offset_max(a) >= high

It is thus not equivalent to \valid(a+(low..high)). Namely, when low > high, \valid(a+(low..high)) is always true, while \valid_range(a,low,high) might not (but is not always false: for instance, if a is a pointer to a single int, i.e.

  \offset_min(a) == \offset_max(a) == 0

then

  • \valid_range(a,0,-42) holds
  • \valid_range(a,42,0) holds
  • \valid_range(a,-1,1) does not hold

A better definition of \valid_range could be

  \valid_range(a,low,high) <==> (low <= high ==> \offset_min(a) <= low && \offset_max(a) >= high)

restoring the equivalence between \valid_range and \valid

mantis/frama-c/issue/156.txt · Last modified: 2009/06/10 17:22 by virgile