[WP] Using Z3 when predicate with access to struct defined leads to inconsistency
Steps to reproduce the issue
Launch the following example with this command (note big timeout):
frama-c -wp -rte -wp-prover="z3" -wp-timeout 100 acsl.c
Example:
struct S
{
int n;
};
/*@ axiomatic Block {
predicate isZero(int left) =
left == 0;
// Unused, but necessary for verification
logic int getN(struct S *s) = s->n;
}*/
/*@ requires \valid(s);
requires isZero(s->n);
assigns \nothing;
ensures \false; // Verified by Z3
*/
void g(struct S *s)
{
}
/*@ assigns \nothing;
ensures \false; // Verified by Z3
*/
void f()
{
struct S s;
s.n = 0;
g(&s);
}
As you can see, specifications establish that f() and g() ensure obviously false statement. The problem is in verification of g(), I've defined f() to show that preconditions of g() can be satisfied.
Expected behaviour
Attempt to prove \false
in postcondition of g()
should fail.
Actual behaviour
Z3 proves \false
in postcondition of g()
:
[kernel] Parsing tmp/acsl/acsl.c (with preprocessing)
[rte:annot] annotating function f
[rte:annot] annotating function g
[wp] Running WP plugin...
[wp] 9 goals scheduled
[wp] Proved goals: 9 / 9
Qed: 7
Z3 4.12.2: 2
Contextual information
- Frama-C installation mode: opam
- Frama-C version: 27.1 (Cobalt)
- Z3 version 4.12.2 - 64 bit
- Why3 platform version: 1.6.0
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 20.04
Additional information
The problem may be in Z3 itself, because Alt-Ergo and CVC4 cannot prove these goals. I've also reproduced the problem using docker image from Docker Hub. I've posted this report as a question on StackOverflow previously (https://stackoverflow.com/questions/77460683/why-wp-with-z3-proves-false-when-access-to-struct-field-is-defined) as I wasn't able to post an issue here.