GitLab

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?