# Admit and check annotations in ACSL

André Maroneze - 10th Jun 2021In Frama-C 23 (Vanadium), two new kinds of ACSL annotations are available, to complement `assert`

: the `admit`

and `check`

annotations. In a nutshell, `assert P`

is equivalent to `check P; admit P`

. The former allows easier checking of the validity of predicates, while the latter documents the introduction of external evidence into a proof. In this blog post, we show a few examples where they may be useful, and also a few pitfalls to avoid.

`admit`

: an `assert`

that is *considered valid*

An `admit`

annotation in ACSL is the same thing as an `assert`

whose status is *Considered valid* (blue/green bullet in the GUI). It is used in situations where Frama-C’s analyzers cannot prove a given property, such as:

- a proof performed by an external tool;
- a paper proof currently out of reach for Frama-C (e.g., complex mathematical invariants on floating-point computations, such as some nonlinear filters);
- the behavior of hardware devices (e.g. registers accessed via absolute addresses);
- the semantics of inline assembly code;
- the specification of complex external functions, whose behavior is more easily modeled using a mix of C code and
`admit`

annotations.

Here’s an example where `admit`

is useful:

```
void main () {
int a = Frama_C_interval(-20000, 20000);
int b = Frama_C_interval(-20000, 20000);
int r = a*a - 2*a*b + b*b;
//@ admit r >= 0;
}
```

Eva cannot currently prove this property by itself; or, to be more precise: Eva *can* prove it, using option `-eva-subdivide-non-linear`

with a sufficiently high value, but this might take a long time in practice.

The next best approach, until Frama-C 22, would be to add an `assert`

with a comment telling the user that the property does hold, even if not proven. This generates unnecessary noise in reports.

With `admit`

, the burden of the proof is shifted to the user; just like in Coq and other tools related to formal proofs, the presence of `admit`

s means the stated property becomes part of the trusted computing base (TCB); `admit`

simply provides a way to clearly document this behavior.

`check`

: evaluate, but do not rely on it

A `check`

is the contrapositive of an `admit`

: it evaluates the predicate validity and emits a status, but does *not* rely on it afterwards. In Eva, for instance, this means the state is *not* reduced. Therefore, unlike `assert`

, `check`

does *not* affect the evaluation and can be inserted without interfering with any analyses.

As an example, consider the effect of adding `assert p != \null`

in some code: it may result in all traces after the `assert`

ignoring the case `p == \null`

. While debugging WP proofs, in particular, such annotations may interfere with the result and complicate understanding; removing them afterwards can once again alter the result of the weakest precondition calculus. With `check`

s, this never happens; you can always include them during debugging, to help understand what’s going on during WP computation.

`admit requires`

, `admit ensures`

, `check requires`

, `check ensures`

Both `admit`

and `check`

can also be used as prefixes to `requires`

and `ensures`

clauses; their behavior is changed in the same way as before. In this case, `check`

is used more often; but a clever developer did find a use for admit ensures.

# When `admit`

is not the right tool

Note that `admit`

does nothing *more* than `assert`

; in particular, it does not allow *introducing* new states and values into an analysis.

For instance, an ACSL beginner’s mistake is to try something like the following code to obtain a non-deterministic range between `min`

and `max`

:

```
// (Should) return the range of integers between [min] and [max]
int nondet_interval(int min, int max) {
int random;
//@ admit \initialized(random) && min <= random <= max;
return random;
}
```

The reason it does not work is that, according to the semantics of C, an uninitialized local variable has an indeterminate value which, in ACSL, can be detected with the `\initialized`

predicate. In the above example, `\initialized(random)`

is false, therefore the annotation is equivalent to `//@ admit \false;`

. The blocking semantics of `admit`

results in an empty state (e.g., `BOTTOM`

in Eva).

If you want to emulate a function such as `Frama_C_interval`

using `admit`

, you may start with a `volatile`

variable; in Eva, the semantics of `volatile int`

is “contains any (initialized) integer”. However, the example below will *still* not work:

```
volatile int random;
int nondet_interval(int min, int max) {
//@ admit min <= random <= max;
return random;
}
```

The problem is unrelated to `admit`

, however! The issue is that `random`

is still `volatile`

, so even after the `admit`

constrained the set of states, the value of `random`

may have been changed (e.g., it could be a register receiving data from the network, with new data arriving just after the evaluation of the `admit`

). Reading the variable again in the `return random`

statement may thus produce *any* value, including those outside `[min; max]`

.

However, if we copy its value into a non-volatile variable, *then* apply the `admit`

, we’ll get the desired behavior:

```
volatile int random;
int nondet_interval(int min, int max) {
int r = random;
//@ admit min <= r <= max;
return r;
}
```

This function does return a value between `min`

and `max`

, without emitting any *Unknown* statuses. It’s not very useful (you should prefer using `Frama_C_interval`

for such situations, since it is already provided in Frama-C’s `__fc_builtin.h`

header), but it illustrates a use case for `admit`

.

# Conclusion

The new ACSL annotations, `admit`

and `check`

, split `assert`

’s functions into fine-grained parts, allowing for better documentation of external semantics and improving debugging of ACSL clauses.

The behavior of `assert`

can be described as `check`

+ `admit`

: *to evaluate a predicate and emit a status* (`check`

), and then *to reduce the set of states after the annotation to those verifying the predicate* (`admit`

).

They also work with `requires`

and `ensures`

: `requires`

is equivalent to `check requires`

followed by `admit requires`

; idem for `ensures`

.

# Acknowledgments

This blog post incorporates suggestions and kind reviews by: Michele Alberti, Patrick Baudin, David Bühler, Maxime Jacquemin, Valentin Perrelle, Julien Signoles.