Known WP limitation: Dynamic allocation is not supported
Hello everyone,
A colleague of mine tried to use variables as a length argument for an array:
int const n = 4;
int main() {
int xs[n];
}
This yielded the following frama-c output:
[nix-shell:~]$ frama-c -wp program.c
[kernel] Parsing program.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] program.c:4: Warning:
Cast with incompatible pointers types (source: sint32*) (target: sint8*)
[wp] program.c:4: Warning:
Cast with incompatible pointers types (source: sint8*) (target: sint32*)
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 1
Frama-c version (for completeness, I'm using the version from nixpkgs unstable):
[nix-shell:~]$ frama-c --version
21.1 (Scandium)
The warning seems strange, as I use only ints in this program. With my limited knowledge of C, I'd say this program does no such casting. Is this a bug or is this somehow a subtle edge case in C? Or is it benign and can it be ignored?