Crash in abstract_interp with an unexpected error when the input program has a syntax error.
Steps to reproduce the issue
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
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)
I reduced the program manually, I can also share the original code or other examples.