Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • 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 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2585

Closed
Open
Created Nov 08, 2021 by arindam-8@arindam-8

Unexpected error (Stack overflow) with large array sizes and expressions

Steps to reproduce the issue

fc-bug.cRun the following command:

frama-c -eva -eva-slevel 100 -eva-plevel 256 -eva-precision 5 -eva-warn-undefined-pointer-comparison pointer -eva-no-alloc-returns-null -warn-signed-overflow -eva-no-show-progress -machdep x86_64 fuzzer-file-102106.c

Expected behaviour

Frama-C when run on the test program with the given command should exit gracefully instead of resulting in an "Unexpected stackoverflow error"

Actual behaviour

When Frama-C is run on the program with the given command parameters it results in a Frama-C crash. with the following trace (abbreviated)

[kernel] Parsing _rmv_fuzzer-file-102106.c (with preprocessing)
[eva] Option -eva-precision 5 detected, automatic configuration of the analysis:
  option -eva-min-loop-unroll set to 0 (default value).
  option -eva-auto-loop-unroll set to 128.
  option -eva-widening-delay set to 3 (default value).
  option -eva-partition-history set to 0 (default value).
  option -eva-slevel already set to 100.
  option -eva-ilevel set to 48.
  option -eva-plevel already set to 256 (not modified).
  option -eva-subdivide-non-linear set to 100.
  option -eva-remove-redundant-alarms set to true (default value).
  option -eva-domains set to 'cvalue,equality,gauges,octagon,symbolic-locations'.
  option -eva-split-return set to 'auto'.
  option -eva-equality-through-calls set to 'formals' (default value).
  option -eva-octagon-through-calls set to false (default value).
[eva] Splitting return states on:
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
  b.f2 ∈ {0}
   .f3 ∈ {65006}
   .[bits 65047 to 65055] ∈ {0}
   .f5 ∈ {65005}
   .[bits 130059 to 130063] ∈ {0}
   .f6 ∈ {-536}
  g.f2 ∈ {65008}
   .f3 ∈ {65000}
   .[bits 65047 to 65055] ∈ {0}
   .f5 ∈ {65005}
   .[bits 130059 to 130063] ∈ {0}
   .f6 ∈ {-536}
  d ∈ {0}
  l ∈ {0}
  a ∈ {0}
  c ∈ {0}
  h ∈ {65008}
  e[0] ∈ {-20}
   [1..65236] ∈ {0}
  f ∈ {{ &d }}
  i[0] ∈ {-533}
   [1..65004] ∈ {0}
  j ∈ {0}
  k ∈ {{ &c }}
[kernel] Current source was: _rmv_fuzzer-file-102106.c:20
  The full backtrace is:
  Raised by primitive operation at file "src/blocks.ml", line 691, characters 11-59
  Called from file "src/blocks.ml", line 703, characters 17-53
  Called from file "src/libraries/utils/wto.ml", line 168, characters 18-36
  Called from file "src/libraries/utils/wto.ml", line 170, characters 34-66

...



  Unexpected error (Stack 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: 22.0 (Titanium)
  • Plug-in used: eva
  • OS name: Ubuntu
  • OS version: Bionic 18.04

Additional information (optional)

The crash seems inconsistent and appears sporadically. It seg-faults on some occasions while on others it crashes like mentioned above. With such expression length issues the crash seems legitimate.

Edited Jan 28, 2022 by Boris Yakobowski
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking