[WP] Soundness issue when handling a pointer on a structure containing an array.
Steps to reproduce the issue
Save the following code into a file called "error.c":
#include <__fc_builtin.h>
struct slice {
int len;
char *buf;
};
int main() {
char b[4] = {0};
struct slice s = {.len = Frama_C_int_interval(2, 100000), .buf=b};
struct slice *p = &s;
//@ assert \valid_read(p->buf + (0..(p->len-1)));
return (int)p->buf[p->len-1];
}
Then analyse this code using the WP plugin with the command
frama-c error.c -eva -wp -wp-rte -wp-prover alt-ergo
Expected behaviour
The assertion //@ assert \valid_read(p->buf + (0..(p->len-1)));
does obviously not hold and should be rejected by WP.
Actual behaviour
The manually added assertion, as well as the RTE assertion generated by wp-rte, are proved by alt-ergo. Using a different prover (z3, cvc4) yields the same result.
Contextual information
- Frama-C installation mode: docker
- Frama-C version: 23.1
- Plug-in used: Eva, WP
- OS name: Ubuntu
- OS version: 20.04
Additional information (optional)
Handling a pointer on a structure containing the array is required to trigger the bug - a simple structure containing the array won't trigger it.
This bug can also be triggered in a slightly more complex setting, where the array access is done in a second function and the assert
clause is replaced by an equivalent requires
clause in the preconditions of that second function.