Frama-c crash with z.Overflow error
Steps to reproduce the issue
No external headers required, just run: (the program is at the end of this report)
frama-c -eva da8af4f574fcb46b5bdc926cec29f39db03d1fb4.c
Expected behaviour
Not to crash. The code is passing compilation with gcc and clang with few warnings.
Actual behaviour
Frama-c crashed:
[kernel] Parsing da8af4f574fcb46b5bdc926cec29f39db03d1fb4.c (with preprocessing)
[kernel] Current source was: da8af4f574fcb46b5bdc926cec29f39db03d1fb4.c:4
The full backtrace is:
Raised by primitive operation at file "src/libraries/stdlib/integer.ml" (inlined), line 100, characters 13-21
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 10006, characters 47-64
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 9976, characters 13-36
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 9697, characters 25-48
Called from file "list.ml", line 121, characters 24-34
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 9687, characters 9-1023
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 9328, characters 10-294
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 10326, characters 12-35
Called from file "list.ml", line 110, characters 12-15
Called from file "src/kernel_internals/typing/cabs2cil.ml", line 10330, characters 2-25
Called from file "src/kernel_internals/typing/frontc.ml", line 83, characters 14-36
Called from file "src/kernel_services/ast_queries/file.ml", line 602, characters 25-44
Called from file "src/kernel_services/ast_queries/file.ml", line 622, characters 14-38
Called from file "src/kernel_services/ast_queries/file.ml", line 685, characters 46-72
Called from file "list.ml", line 121, characters 24-34
Called from file "src/kernel_services/ast_queries/file.ml", line 685, characters 17-89
Called from file "src/kernel_services/ast_queries/file.ml", line 1625, characters 24-60
Called from file "src/kernel_services/ast_queries/file.ml", line 1702, characters 4-27
Called from file "src/kernel_services/ast_data/ast.ml", line 110, characters 2-28
Called from file "src/kernel_services/ast_data/ast.ml", line 118, characters 53-71
Called from file "src/kernel_internals/runtime/boot.ml", line 29, characters 6-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 (Z.Overflow).
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 is 21.0 (Scandium) and Frama-C version is 22.0 (Titanium)
- Plug-in used: eva
- OS name: Ubuntu
- OS version: 18
Additional information (optional)
I reduced the program that crashed Frama-c into this: (via Creduce)
long a;
void b() {
switch (a)
case 0 ... 9999999999999999999:;
}
void main() {}