In 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 admits 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 checks, 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.