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.