GitLab

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

Additional information (optional)