[EVA] unsoundness when initializing in switch statement before first case
Steps to reproduce the issue
The following code is validated by EVA:
#include <stdio.h>
int main(int argc, char *argv[]) {
switch(argc) {
int i = 5;
case 0:
i = 17;
// fall-through
default:
//@ assert i == 17;
printf("%d\n", i);
}
return 0;
}
The file is run through frama-c:
frama-c -eva test.c
Expected behaviour
Eva should not validate the assert, since "i" is possibly uninitialized. This is because in C, code between the switch statement and the first case is not executed. Note that frama-c-gui correctly shows that code as dead code.
Actual behaviour
Eva validates the assert. No warnings are generated.
Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 27.1 (Cobalt)
- Plug-in used: Eva
- OS name: Ubuntu
- OS version: 22.04
Additional information (optional)
When using -slevel 2
or above, Eva does not validate the assert, but still validates the generated \initialized
assert for printf
.
If int i
is not initialized before the first case, Eva does not validate the assert. If a break
is inserted, it does not validate the assert either.