frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2022-10-24T14:54:46Zhttps://git.frama-c.com/pub/frama-c/-/issues/2574Frama-c fails parsing gcc/llvm single source test case with typedef depended ...2022-10-24T14:54:46ZKarine EMFrama-c fails parsing gcc/llvm single source test case with typedef depended on function's parameter<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
```
frama-c 20040411-1.c
```
### Expected behaviour
<!--
Please explain here what is the 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
<!--
Please explain here what is the actual (faulty) 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)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2573Frama-c fails parsing gcc/llvm single source test case (exit with "invalid us...2022-07-11T16:12:43ZKarine EMFrama-c fails parsing gcc/llvm single source test case (exit with "invalid user input")<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### 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
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
<!--
Please explain here what is the 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
<!--
Please explain here what is the actual (faulty) 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)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
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;
}
```Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2559No support for complex numbers via the keyword _Complex2022-04-27T15:22:34ZKarine EMNo support for complex numbers via the keyword _Complex<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Frama-c does not support complex numbers via the keyword _Complex for C code.
See here: https://gcc.gnu.org/onlinedocs/gcc-4.1.2/gcc/Complex.html
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
When running this code:
```
float _Complex f;
int main () { }
```
Frama-c returns an error:
```
[kernel] Parsing test12.c (with preprocessing) [kernel] test12.c:1:
syntax error:
Location: line 1, between columns 6 and 15, before or at token: f
1 float _Complex f;
^^^^^^^^^^^^^^^^^
2 int main () { }
[kernel] Frama-C aborted: invalid user input.
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: *Frama-C version* (as reported by `frama-c -version`) 22\.0 (Titanium)
- Plug-in used: -eva
- OS name: Ubuntu
- OS version: 18
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
We use Frama-c to automatically analyse code from llvm and gcc test-suites; some of the programs triggered this error message.
I reduced the code but I can add the link to the original one.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2555Crash in abstract_interp with an unexpected error when the input program has ...2021-05-21T09:25:42ZKarine EMCrash in abstract_interp with an unexpected error when the input program has a syntax error.<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
The following program has a syntax error that crashed frama-c instead of returning an alarm.
E.g., gcc returns the following compile-time error:
```
user42@srg08:~/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/Frama-C-zone$ gcc -w 0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c
0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c:10:11: error: negative width in bit-field ‘b’
10 | int32_t b:(-19);
|
```
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
The following code crashed frama-c:
```
user42@srg08:~/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/Frama-C-zone$ more 0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c
#if __SIZEOF_INT__ < 4
__extension__ typedef __INT32_TYPE__ int32_t;
#else
typedef int int32_t;
#endif
#pragma pack(1)
struct S
{
int32_t b:(-19);
} i;
int main ()
{
return (-1);
}
```
with the following error:
```
user42@srg08:~/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/Frama-C-zone$ frama-c -eva 0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c
[kernel] Parsing 0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[kernel] Current source was: 0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c:11
The full backtrace is:
Raised at file "src/kernel_services/abstract_interp/base.ml", line 217, characters 2-27
Called from file "src/kernel_services/abstract_interp/base.ml", line 480, characters 17-43
Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22
Called from file "src/plugins/value/domains/cvalue/cvalue_domain.ml", line 394, characters 15-38
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/domains/cvalue/cvalue_domain.ml", line 405, characters 4-34
Called from file "src/plugins/value/engine/initialization.ml", line 309, characters 16-68
Called from file "list.ml", line 121, characters 24-34
Called from file "src/kernel_services/ast_data/globals.ml" (inlined), line 128, characters 33-72
Called from file "src/plugins/value/engine/initialization.ml", line 324, characters 15-65
Called from file "src/libraries/project/state_builder.ml", line 403, characters 17-21
Called from file "src/plugins/value/engine/initialization.ml", line 396, characters 20-43
Called from file "src/plugins/value/engine/compute_functions.ml", line 357, characters 10-55
Called from file "src/libraries/project/state_builder.ml", line 994, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1002, characters 9-18
Called from file "src/plugins/value/register.ml", line 39, characters 46-66
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 842, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 872, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 231, characters 4-8
Unexpected error (File "src/kernel_services/abstract_interp/base.ml", line 217, characters 2-8: Assertion failed).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 22.0 (Titanium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: *Frama-C version* (as reported by `frama-c -version`) 22.0 (Titanium)
- Plug-in used: -eva
- OS name: Ubuntu
- OS version: 18
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
I reduced the program manually, I can also share the original code or other examples.Andre MaronezeAndre Maroneze