GitLab

Steps to reproduce the issue

frama-c 20040411-1.c

Expected behaviour

Frama-c cannot parse the following C single source test case from GCC/LLVM test suite. https://github.com/llvm/llvm-test-suite/blob/main/SingleSource/Regression/C/gcc-c-torture/execute/20040411-1.c and gcc and llvm seem to be able to compile the program:

gcc A_20040411-1.c
A_20040411-1.c: In function ‘sub1’:
A_20040411-1.c:10:7: warning: implicit declaration of function ‘memcpy’ [-Wimplicit-function-declaration]
   10 |       memcpy (x, y, 10 * sizeof (int));
      |       ^~~~~~
A_20040411-1.c:10:7: warning: incompatible implicit declaration of built-in function ‘memcpy’
A_20040411-1.c:1:1: note: include ‘<string.h>’ or provide a declaration of ‘memcpy’
  +++ |+#include <string.h>
    1 | /* corpus/20040411-1.c */
A_20040411-1.c: In function ‘main’:
A_20040411-1.c:20:7: warning: implicit declaration of function ‘abort’ [-Wimplicit-function-declaration]
   20 |     { abort (); }
      |       ^~~~~
A_20040411-1.c:20:7: warning: incompatible implicit declaration of built-in function ‘abort’
A_20040411-1.c:1:1: note: include ‘<stdlib.h>’ or provide a declaration of ‘abort’
  +++ |+#include <stdlib.h>
    1 | /* corpus/20040411-1.c */
./a.out

clang-12 A_20040411-1.c
A_20040411-1.c:10:7: warning: implicitly declaring library function 'memcpy' with type 'void *(void *, const void *, unsigned long)' [-Wimplicit-function-declaration]
      memcpy (x, y, 10 * sizeof (int));
      ^
A_20040411-1.c:10:7: note: include the header <string.h> or explicitly provide a declaration for 'memcpy'
A_20040411-1.c:20:7: warning: implicitly declaring library function 'abort' with type 'void (void) __attribute__((noreturn))' [-Wimplicit-function-declaration]
    { abort (); }
      ^
A_20040411-1.c:20:7: note: include the header <stdlib.h> or explicitly provide a declaration for 'abort'
2 warnings generated.
./a.out

Actual behaviour

Frama-c exit with the following error:

[kernel] Parsing /home/user42/directed-compiler-fuzzing-code/scripts/7-diff-testing/results_output/A_20040411-1.c (with preprocessing)
[kernel] /home/user42/directed-compiler-fuzzing-code/scripts/7-diff-testing/results_output/A_20040411-1.c:5: User Error: 
  Array length i + 2 is not a compile-time constant.
[kernel:typing:implicit-function-declaration] /home/user42/directed-compiler-fuzzing-code/scripts/7-diff-testing/results_output/A_20040411-1.c:10: Warning: 
  Calling undeclared function memcpy. Old style K&R code?
[kernel:typing:implicit-function-declaration] /home/user42/directed-compiler-fuzzing-code/scripts/7-diff-testing/results_output/A_20040411-1.c:20: Warning: 
  Calling undeclared function abort. Old style K&R code?
[kernel] User Error: stopping on
  file "/home/user42/directed-compiler-fuzzing-code/scripts/7-diff-testing/results_output/A_20040411-1.c"
  that has errors. Add '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.

Contextual information

• Frama-C installation mode: Opam 4.10.0
• Frama-C version: 22.0 (Titanium)
• Plug-in used: Plug-in used
• OS name: Ubuntu
• OS version: 18

Additional information (optional)