https://gcc.gnu.org/bugzilla/show_bug.cgi?id=64269
--- Comment #2 from Markus Trippelsdorf <trippels at gcc dot gnu.org> --- But the testcase is invalid: markus@x4 tmp % frama-c -val -val-signed-overflow-alarms -precise-unions -obviously-terminates -no-val-show-progress -machdep x86_64 test_case_7213.c [kernel] preprocessing with "gcc -C -E -I. test_case_7213.c" [value] Analyzing a complete application starting at main [value] Computing initial state [value] Initial state computed [value] Values of globals at initialization test_case_7213.c:14:[kernel] warning: out of bounds write. assert \valid(tmp_5);