GitLab

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-bugs

Expected 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