GitLab

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.