GitLab

Steps to reproduce the issue

frama-c -eva with the following program:

#include <string.h>
int main (void)
{
  void *x; 
  memset (x, 0, 2 * 4);
  return 0;
}

Expected behaviour

Not to crash.

Actual behaviour

Crash with this error:

 frama-c -eva ../../9-reduce-bugs/crash-frama-c/9-error-Not_found/6185ea1b8f1da01180c959fe26694bb58e3d3241_reduced.c
[kernel] Parsing /home/user42/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/crash-frama-c/9-error-Not_found/6185ea1b8f1da01180c959fe26694bb58e3d3241_reduced.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[eva:alarm] /home/user42/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/crash-frama-c/9-error-Not_found/6185ea1b8f1da01180c959fe26694bb58e3d3241_reduced.c:5: Warning:
  function memset: precondition 'valid_s' got status unknown.
[eva] FRAMAC_SHARE/libc/string.h:118:
  cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
[kernel] Current source was: /home/user42/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/crash-frama-c/9-error-Not_found/6185ea1b8f1da01180c959fe26694bb58e3d3241_reduced.c:5
  The full backtrace is:
  Raised at file "src/kernel_services/abstract_interp/map_lattice.ml", line 220, characters 14-29
  Called from file "src/kernel_services/abstract_interp/map_lattice.ml", line 230, characters 25-42
  Called from file "src/kernel_services/abstract_interp/map_lattice.ml", line 237, characters 25-42
  Called from file "src/plugins/value/domains/cvalue/builtins_memory.ml", line 580, characters 35-73
  Called from file "src/plugins/value/domains/cvalue/builtins_memory.ml", line 634, characters 10-61
  Called from file "src/plugins/value/domains/cvalue/builtins.ml", line 253, characters 6-27
  Called from file "src/plugins/value/domains/cvalue/builtins.ml", line 268, characters 12-54
  Called from file "src/plugins/value/engine/compute_functions.ml", line 304, characters 10-65
  Called from file "src/plugins/value/engine/transfer_stmt.ml", line 318, characters 10-43
  Called from file "src/plugins/value/engine/transfer_stmt.ml", line 456, characters 22-60
  Called from file "src/plugins/value/engine/transfer_stmt.ml", line 758, characters 26-75
  Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
  Called from file "src/plugins/value/engine/transfer_stmt.ml", line 754, characters 10-447
  Called from file "list.ml", line 121, characters 24-34
  Called from file "src/plugins/value/engine/transfer_stmt.ml", line 769, characters 24-59
  Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
  Called from file "src/plugins/value/engine/transfer_stmt.ml", line 742, characters 6-1023
  Called from file "src/plugins/value/engine/iterator.ml", line 274, characters 6-47
  Called from file "src/plugins/value/partitioning/partition.ml", line 494, characters 29-34
  Called from file "list.ml", line 121, characters 24-34
  Called from file "src/plugins/value/engine/iterator.ml", line 430, characters 15-71
  Called from file "src/plugins/value/engine/iterator.ml", line 494, characters 18-35
  Called from file "list.ml", line 92, characters 20-23
  Called from file "src/plugins/value/engine/iterator.ml", line 496, characters 18-60
  Called from file "src/plugins/value/engine/iterator.ml", line 543, characters 13-31
  Called from file "list.ml", line 110, characters 12-15
  Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 540, characters 4-31
  Called from file "src/plugins/value/engine/iterator.ml", line 602, characters 6-22
  Called from file "src/plugins/value/engine/iterator.ml", line 769, characters 20-39
  Called from file "src/plugins/value/engine/compute_functions.ml", line 201, characters 8-45
  Called from file "src/plugins/value/engine/compute_functions.ml", line 333, characters 25-75
  Called from file "src/libraries/project/state_builder.ml", line 994, characters 9-13
  Re-raised at file "src/libraries/project/state_builder.ml", line 1002, characters 9-18
  Called from file "src/plugins/value/register.ml", line 39, characters 46-66
  Called from file "queue.ml", line 121, characters 6-15
  Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 842, characters 2-9
  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 872, characters 18-64
  Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 231, characters 4-8
  Unexpected error (Not_found).
  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: 18

Additional information (optional)

This is program compiles but got runtime errors, I would expect frama-c to give a warning. It seems like it crashed when analysing the memset line.