Eva plugin crashed with program calling memset
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.