Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2588

Closed
Open
Created Dec 17, 2021 by Karine EM@karineek

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

Additional information (optional)

Edited Dec 17, 2021 by Karine EM
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking