GitLab

Steps to reproduce the issue

frama-c pr85169.c

see the code below or get from here: https://github.com/llvm/llvm-test-suite/blob/main/SingleSource/Regression/C/gcc-c-torture/execute/pr85169.c

Expected behaviour

I tried to run frama-c on one of the GCC/LLVM single source test case which passes compilation with both compilers. I expected Frama-c to also pass the parsing stage.

gcc /home/user42/directed-compiler-fuzzing-code/scripts/1-general-utils/testme_07092021-processed.ubfree.ubfree/A_pr85169_copy.c
./a.out
clang /home/user42/directed-compiler-fuzzing-code/scripts/1-general-utils/testme_07092021-processed.ubfree.ubfree/A_pr85169_copy.c
/home/user42/directed-compiler-fuzzing-code/scripts/1-general-utils/testme_07092021-processed.ubfree.ubfree/A_pr85169_copy.c:7:29: warning: unknown attribute 'noipa' ignored [-Wunknown-attributes]
static void __attribute__ ((noipa))
                            ^~~~~
1 warning generated.
./a.out

Actual behaviour

Frama-c cannot parse the program; /tmp/A_pr85169_copy.c04c2b1.i exists and passes compilation with gcc. Exit with this error:

user42@srg08:~/directed-compiler-fuzzing-code/scripts/7-diff-testing/Frama-C-zone$ frama-c ../../1-general-utils/testme_07092021-processed.ubfree.ubfree/A_pr85169_copy.c -kernel-msg-key pp
[kernel:pp]
  preprocessing with "gcc -E -C -I.  -I/home/user42/.opam/4.10.0/share/frama-c/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 '/home/user42/directed-compiler-fuzzing-code/scripts/1-general-utils/testme_07092021-processed.ubfree.ubfree/A_pr85169_copy.c' -o '/tmp/A_pr85169_copy.c04c2b1.i'"
[kernel] Parsing /home/user42/directed-compiler-fuzzing-code/scripts/1-general-utils/testme_07092021-processed.ubfree.ubfree/A_pr85169_copy.c (with preprocessing)
[kernel] /home/user42/directed-compiler-fuzzing-code/scripts/1-general-utils/testme_07092021-processed.ubfree.ubfree/A_pr85169_copy.c:11: Failure:
  Expecting exactly one pointer type in array access v[63] (V and int)
[kernel] User Error: stopping on
  file "/home/user42/directed-compiler-fuzzing-code/scripts/1-general-utils/testme_07092021-processed.ubfree.ubfree/A_pr85169_copy.c"
  that has errors.
[kernel] Frama-C aborted: invalid user input.

Contextual information

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

Additional information (optional)

The program is taken from here: https://github.com/llvm/llvm-test-suite/blob/main/SingleSource/Regression/C/gcc-c-torture/execute/pr85169.c, and it is this one:

user42@srg08:~/directed-compiler-fuzzing-code/scripts/7-diff-testing/Frama-C-zone$ more /home/user42/directed-compiler-fuzzing-code/scripts/1-general-utils/testme_07092021-processed.ubfree.ubfree/A_pr85169_copy.c
/* PR target/85169 */
typedef char V __attribute__((vector_size (64)));
static void __attribute__ ((noipa))
foo (V *p)
{
  V v = *p;
  v[63] = 1;
  *p = v;
}
int main()
{
  V v = (V) { };
  foo (&v);
  for (unsigned i = 0; i < 64; i++) {
    if (v[i] != (i == 63))
    { __builtin_abort (); }
    }
  return 0;
}