Skip to content

GitLab

  • Menu
Projects Groups 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
    • Contributors
    • Graph
    • Compare
  • Issues 201
    • Issues 201
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • 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
  • #2550
Closed
Open
Created Apr 06, 2021 by Karine EM@karineek

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() {}
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking