For Frama-C and the WP plugin, how can a user assert that a point in a program is unreachable?
Looking for something like:
//@ assert \unreachable;
You can use //@ assert \false;
for an assertion that a point is unreachable because:
a (provably) unreachable assertion is always proved to be true
via Introduction to C program proof with Frama-C and its WP plugin by Allan Blanchard.
e.g. For a given file main.c
:
/*@
assigns \nothing;
*/
int foo(const int input) {
int result = 0;
if (input > 0) {
result += 1;
if (input < 0) {
// This assertion will be proved successfully
// because this location is provably unreachable.
//@ assert \false;
result += 1;
}
}
return result;
}
To verify that the assertion is proved:
$ frama-c -wp main.c
[kernel] Parsing main.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
[wp] Proved goals: 3 / 3
Qed: 3
The above is using frama-c
version 25.0 (Manganese).