development version
ID0002502: This issue was created automatically from Mantis Issue 2502. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002502 | Frama-C | Plug-in > Eva | public | 2020-03-12 | 2020-06-12 |
| Reporter | puccetti2 | Assigned To | buhler | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | MacOS X | OS | - | OS Version | 10.15.3 |
| Product Version | Frama-C 19-Potassium | Target Version | - | Fixed in Version | Frama-C 21-Scandium |
Description :
Running EVA on the small example leads to a cash
Additional Information :
$ frama-c max_array2.c -val
[kernel] Parsing max_array2.c (with preprocessing)
[kernel:parser:decimal-float] max_array2.c:26: Warning:
Floating-point constant 4.6 is not represented exactly. Will use 0x1.2666666666666p2.
(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
[eva:alarm] max_array2.c:28: Warning:
function max_array: precondition ∀ ℤ j;
0 ≤ j < n ⇒ \valid_read(t + j) got status unknown.
[kernel] Current source was: max_array2.c:15
The full backtrace is:
Raised at file "src/plugins/value/legacy/eval_terms.ml", line 1264, characters 9-21
Called from file "src/plugins/value/legacy/eval_terms.ml", line 1030, characters 13-41
Called from file "src/plugins/value/legacy/eval_terms.ml", line 2127, characters 18-66
Called from file "src/plugins/value/legacy/eval_terms.ml", line 2308, characters 4-20
Called from file "src/plugins/value/domains/cvalue/cvalue_domain.ml", line 284, characters 10-49
Called from file "src/plugins/value/engine/transfer_logic.ml", line 663, characters 25-61
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/transfer_logic.ml", line 660, characters 10-488
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 377, characters 8-69
Called from file "src/plugins/value/engine/iterator.ml", line 381, characters 17-61
Called from file "src/plugins/value/engine/partition.ml", line 481, characters 29-34
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 469, characters 8-57
Called from file "src/plugins/value/engine/iterator.ml", line 556, characters 12-45
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 542, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 604, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 774, characters 20-39
Called from file "src/plugins/value/engine/compute_functions.ml", line 210, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 230, characters 26-36
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 307, characters 10-43
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 445, characters 22-60
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 749, 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 745, characters 10-447
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 760, 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 733, characters 6-1023
Called from file "src/plugins/value/engine/iterator.ml", line 277, characters 6-47
Called from file "src/plugins/value/engine/partition.ml", line 481, 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 496, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 498, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 545, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 542, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 604, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 774, characters 20-39
Called from file "src/plugins/value/engine/compute_functions.ml", line 210, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 343, 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 792, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
Unexpected error (File "src/plugins/value/legacy/eval_terms.ml", line 1264, characters 9-15: Assertion failed).
Steps To Reproduce :
frama-c-gui max_array2.c -val