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.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information