GitLab

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() {}