Unexpected error (File "src/plugins/value/engine/evaluation.ml", line 1176, characters 14-20: Assertion failed)
Steps to reproduce the issue
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 test.c
with this test case:
struct a c;
struct a {
unsigned b;
} d(struct a *e, unsigned f) {
g(e);
0 - e->b * -((long)f >> (int)e->b >> 3 * f - e->b) * -e->b - (int)e;
}
main() { d(&c, 55); }will crash with this error:
[kernel] Parsing fuzzer-file-17090.c (with preprocessing)
[kernel:typing:implicit-function-declaration] fuzzer-file-17090.c:5: Warning:
Calling undeclared function g. Old style K&R code?
[kernel:CERT:MSC:37] fuzzer-file-17090.c:6: Warning:
Body of function d falls-through. Adding a return statement
[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
c ∈ {0}
[kernel:annot:missing-spec] fuzzer-file-17090.c:5: Warning:
Neither code nor specification for function g, generating default assigns from the prototype
[eva] using specification for function g
[kernel] Current source was: fuzzer-file-17090.c:6
The full backtrace is:
Raised at Evaluation.Make.find_val in file "src/plugins/value/engine/evaluation.ml", line 1176, characters 14-26
Called from Evaluation.Make.internal_backward.(fun) in file "src/plugins/value/engine/evaluation.ml", line 1301, characters 6-17
Called from Evaluation.Make.internal_backward.(fun) in file "src/plugins/value/engine/evaluation.ml", line 1307, characters 6-36
Called from Evaluation.Make.evaluate.(fun) in file "src/plugins/value/engine/evaluation.ml", line 1534, characters 8-56
Called from Bottom.Type.(>>-) in file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
Called from Evaluation.Make.evaluate in file "src/plugins/value/engine/evaluation.ml", line 1532, characters 8-163
Called from Transfer_stmt.Make.evaluate_and_check in file "src/plugins/value/engine/transfer_stmt.ml", line 164, characters 14-59
Called from Transfer_stmt.Make.assign_by_eval in file "src/plugins/value/engine/transfer_stmt.ml", line 184, characters 4-54
Called from Transfer_stmt.Make.assign_lv_or_ret in file "src/plugins/value/engine/transfer_stmt.ml", line 258, characters 10-55
Called from Initialization.Make.apply_cil_single_initializer in file "src/plugins/value/engine/initialization.ml", line 131, characters 10-48
Called from Initialization.Make.initialize_local_variable in file "src/plugins/value/engine/initialization.ml", line 304, characters 8-95
Called from Iterator.Make_Dataflow.lift' in file "src/plugins/value/engine/iterator.ml", line 234, characters 33-36
Called from Partition.MakeFlow.transfer.transfer in file "src/plugins/value/partitioning/partition.ml", line 649, characters 29-42
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Iterator.Make_Dataflow.process_edge in file "src/plugins/value/engine/iterator.ml", line 436, characters 15-74
Called from Iterator.Make_Dataflow.process_vertex.process_source in file "src/plugins/value/engine/iterator.ml", line 501, characters 18-35
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Iterator.Make_Dataflow.process_vertex in file "src/plugins/value/engine/iterator.ml", line 503, characters 18-60
Called from Iterator.Make_Dataflow.iterate_element in file "src/plugins/value/engine/iterator.ml", line 550, characters 13-31
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Iterator.Make_Dataflow.iterate_list in file "src/plugins/value/engine/iterator.ml" (inlined), line 547, characters 4-31
Called from Iterator.Make_Dataflow.compute in file "src/plugins/value/engine/iterator.ml", line 609, characters 6-22
Called from Iterator.Computer.compute.compute in file "src/plugins/value/engine/iterator.ml", line 776, characters 20-39
Called from Value_util.protect in file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from Compute_functions.Make.compute_using_spec_or_body in file "src/plugins/value/engine/compute_functions.ml", line 206, characters 8-45
Called from Compute_functions.Make.compute_and_cache_call in file "src/plugins/value/engine/compute_functions.ml", line 228, characters 26-36
Called from Transfer_stmt.Make.process_call.process in file "src/plugins/value/engine/transfer_stmt.ml", line 326, characters 10-53
Called from Value_util.protect in file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from Transfer_stmt.Make.do_one_call in file "src/plugins/value/engine/transfer_stmt.ml", line 463, characters 22-70
Called from Transfer_stmt.Make.call.(fun).process_one_function.(fun) in file "src/plugins/value/engine/transfer_stmt.ml", line 767, characters 14-73
Called from Bottom.Type.(>>-:) in file "src/kernel_services/abstract_interp/bottom.ml", line 36, characters 25-30
Called from Transfer_stmt.Make.call.(fun).process_one_function in file "src/plugins/value/engine/transfer_stmt.ml", line 762, characters 12-489
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Bottom.Type.(>>-:) in file "src/kernel_services/abstract_interp/bottom.ml", line 36, characters 25-30
Called from Transfer_stmt.Make.call in file "src/plugins/value/engine/transfer_stmt.ml", line 749, characters 6-1023
Called from Iterator.Make_Dataflow.transfer_call in file "src/plugins/value/engine/iterator.ml", line 278, characters 6-47
Called from Partition.MakeFlow.transfer.transfer in file "src/plugins/value/partitioning/partition.ml", line 649, characters 29-42
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Iterator.Make_Dataflow.process_edge in file "src/plugins/value/engine/iterator.ml", line 436, characters 15-74
Called from Iterator.Make_Dataflow.process_vertex.process_source in file "src/plugins/value/engine/iterator.ml", line 501, characters 18-35
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Iterator.Make_Dataflow.process_vertex in file "src/plugins/value/engine/iterator.ml", line 503, characters 18-60
Called from Iterator.Make_Dataflow.iterate_element in file "src/plugins/value/engine/iterator.ml", line 550, characters 13-31
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Iterator.Make_Dataflow.iterate_list in file "src/plugins/value/engine/iterator.ml" (inlined), line 547, characters 4-31
Called from Iterator.Make_Dataflow.compute in file "src/plugins/value/engine/iterator.ml", line 609, characters 6-22
Called from Iterator.Computer.compute.compute in file "src/plugins/value/engine/iterator.ml", line 776, characters 20-39
Called from Value_util.protect in file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from Compute_functions.Make.compute_using_spec_or_body in file "src/plugins/value/engine/compute_functions.ml", line 206, characters 8-45
Called from Compute_functions.Make.compute.compute in file "src/plugins/value/engine/compute_functions.ml", line 344, characters 8-63
Called from Value_util.protect in file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from Analysis.force_compute in file "src/plugins/value/engine/analysis.ml", line 181, characters 2-49
Called from State_builder.apply_once.(fun) in file "src/libraries/project/state_builder.ml", line 998, characters 9-13
Re-raised at State_builder.apply_once.(fun) in file "src/libraries/project/state_builder.ml", line 1006, characters 9-18
Called from Register.main in file "src/plugins/value/register.ml", line 39, characters 46-66
Called from Stdlib__Queue.iter.iter in file "queue.ml", line 121, characters 6-15
Called from Boot.play_analysis in file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 846, characters 2-9
Called from Cmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 876, characters 18-64
Called from Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 235, characters 4-8
Unexpected error (File "src/plugins/value/engine/evaluation.ml", line 1176, characters 14-20: Assertion failed).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 24.0 (Chromium).
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-bugsExpected behaviour
Not to crash
Actual behaviour
Crashed with this error
Unexpected error (File "src/plugins/value/engine/evaluation.ml", line 1176, characters 14-20: Assertion failed).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 24.0 (Chromium).Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 24.0 (Chromium)
- Plug-in used: eva
- OS name: Unix Ubuntu
- OS version: 18.04 LTS
Additional information (optional)
This is a fuzzed + reduced program