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

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

mantis:frama-c:issue:156

This page details the semantics of ACSL `\valid`

predicate related to
Issue ~~Mantis:156~~ in the BTS.

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

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.

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.

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.

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