Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 177
    • Issues 177
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2573

Frama-c fails parsing gcc/llvm single source test case (exit with "invalid user input")

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;
}
Edited Sep 14, 2021 by Karine EM
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking