Frama-c crashes with "src/kernel_services/abstract_interp/ival.ml", line 444, characters 31-37: Assertion failed
Steps to reproduce the issue
frama-c -eva fuzzer-file-49652.c
Expected behaviour
Not to crash
Actual behaviour
Frama-c 24.0 crashed with "src/kernel_services/abstract_interp/ival.ml", line 444, characters 31-37: Assertion failed
I reduced the original program to this:
#include <stdarg.h>
long a;
void b(va_list ap) {
a = va_arg(ap, double);
a += va_arg(ap, long);
}
void c(int d, ...) {
va_list ap;
va_start(ap, d);
b(ap);
}
void main() { c(0, 8.1, 7.1); }
The crash's trace is:
[kernel] Parsing fuzzer-file-49652.c (with preprocessing)
[kernel:parser:decimal-float] fuzzer-file-49652.c:12: Warning:
Floating-point constant 7.1 is not represented exactly. Will use 0x1.c666666666666p2.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
a ∈ {0}
[eva:alarm] fuzzer-file-49652.c:5: Warning:
signed overflow. assert a + tmp ≤ 9223372036854775807;
(tmp from vararg)
[kernel] Current source was: fuzzer-file-49652.c:5
The full backtrace is:
Raised at file "src/kernel_services/abstract_interp/ival.ml", line 444, characters 31-43
Called from file "src/libraries/utils/hptmap.ml", line 934, characters 18-24
Called from file "src/kernel_services/abstract_interp/map_lattice.ml", line 428, characters 24-39
Called from file "src/plugins/value_types/cvalue.ml", line 557, characters 10-64
Called from file "src/plugins/value/legacy/eval_terms.ml", line 1357, characters 17-46
Called from file "src/plugins/value/legacy/eval_terms.ml" (inlined), line 2680, characters 25-57
Called from file "src/plugins/value/legacy/eval_terms.ml", line 2690, characters 22-36
Called from file "src/plugins/value/legacy/eval_terms.ml", line 2736, characters 11-29
Called from file "src/plugins/inout/operational_inputs.ml", line 383, characters 19-67
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/inout/operational_inputs.ml", line 485, characters 6-28
Called from file "src/kernel_services/analysis/dataflows.ml", line 514, characters 12-42
Called from file "src/kernel_services/analysis/dataflows.ml", line 522, characters 19-30
Called from file "src/kernel_services/analysis/dataflows.ml", line 523, characters 5-14
Called from file "src/kernel_services/analysis/dataflows.ml" (inlined), line 582, characters 10-48
Called from file "src/kernel_services/analysis/dataflows.ml" (inlined), line 582, characters 10-57
Called from file "src/kernel_services/analysis/dataflows.ml", line 582, characters 10-60
Called from file "src/plugins/inout/operational_inputs.ml" (inlined), line 702, characters 6-37
Called from file "src/plugins/inout/operational_inputs.ml", line 702, characters 6-48
Called from file "src/plugins/inout/operational_inputs.ml", line 716, characters 14-78
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/plugins/value/engine/iterator.ml", line 731, characters 8-214
Called from file "src/plugins/value/engine/iterator.ml", line 780, characters 6-31
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/compute_functions.ml", line 206, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 228, characters 26-36
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 326, characters 10-53
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 463, characters 22-70
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 767, characters 14-73
Called from file "src/kernel_services/abstract_interp/bottom.ml", line 36, characters 25-30
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 762, characters 12-489
Called from file "list.ml", line 121, characters 24-34
Called from file "src/kernel_services/abstract_interp/bottom.ml", line 36, characters 25-30
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 749, characters 6-1023
Called from file "src/plugins/value/engine/iterator.ml", line 278, characters 6-47
Called from file "src/plugins/value/partitioning/partition.ml", line 649, characters 29-42
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 436, characters 15-74
Called from file "src/plugins/value/engine/iterator.ml", line 501, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 503, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 550, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 547, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 609, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 776, characters 20-39
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/compute_functions.ml", line 206, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 228, characters 26-36
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 326, characters 10-53
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 463, characters 22-70
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 767, characters 14-73
Called from file "src/kernel_services/abstract_interp/bottom.ml", line 36, characters 25-30
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 762, characters 12-489
Called from file "list.ml", line 121, characters 24-34
Called from file "src/kernel_services/abstract_interp/bottom.ml", line 36, characters 25-30
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 749, characters 6-1023
Called from file "src/plugins/value/engine/iterator.ml", line 278, characters 6-47
Called from file "src/plugins/value/partitioning/partition.ml", line 649, characters 29-42
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 436, characters 15-74
Called from file "src/plugins/value/engine/iterator.ml", line 501, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 503, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 550, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 547, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 609, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 776, characters 20-39
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/compute_functions.ml", line 206, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 344, characters 8-63
Called from file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from file "src/plugins/value/engine/analysis.ml", line 181, characters 2-49
Called from file "src/libraries/project/state_builder.ml", line 998, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1006, 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 846, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 876, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 235, characters 4-8
Unexpected error (File "src/kernel_services/abstract_interp/ival.ml", line 444, characters 31-37: 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
Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 24.0 (Chromium)
- Plug-in used: eva
- OS name: Ubuntu
- OS version: 18.04