View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002502 | Frama-C | Plug-in > Eva | public | 2020-03-12 15:20 | 2020-06-12 08:59 | ||||
Reporter | puccetti2 | ||||||||
Assigned To | buhler | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Platform | MacOS X | OS | OS Version | 10.15.3 | |||||
Product Version | Frama-C 19-Potassium | ||||||||
Target Version | Fixed in Version | Frama-C 21-Scandium | |||||||
Summary | 0002502: development version | ||||||||
Description | Running EVA on the small example leads to a cash | ||||||||
Steps To Reproduce | frama-c-gui max_array2.c -val | ||||||||
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). | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
maroneze (administrator) 2020-03-17 13:59 |
Thanks for the report. Fixed in commit 4a4685f3 (Frama-C development branch). The fixed version allows the user to realize that the loop invariant in the provided code is invalid, and should be: /*@ loop invariant 0 <= i <= n && (m == \max(0,i-1,\lambda integer k; t[k])); |
maroneze (administrator) 2020-03-17 14:00 |
Fixed in commit 4a4685f3 |
buhler (developer) 2020-03-17 14:47 |
In ACSL, \max(i, j, f) is unspecified when i>j, so in the example, a loop invariant with \max(0,i-1,…) should never be proved. Instead, you can use : /*@ loop invariant 0 <= i <= n && (i == 0 || m == \max(0,i,\lambda integer k; t[k])); */ Or simply initialize the variable m to t[0]. In both cases, the example should be proved with Eva by using option -eva-auto-loop-unroll 10. However, note that Eva precisely evaluates \max(i, j, f) only if i-j <= 10. Otherwise, imprecise over-approximations are made. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2020-03-12 15:20 | puccetti2 | New Issue | |
2020-03-12 15:20 | puccetti2 | Status | new => assigned |
2020-03-12 15:20 | puccetti2 | Assigned To | => buhler |
2020-03-12 15:20 | puccetti2 | File Added: max_array2.c | |
2020-03-17 11:13 | maroneze | Additional Information Updated | View Revisions |
2020-03-17 13:59 | maroneze | Note Added: 0006962 | |
2020-03-17 14:00 | maroneze | Note Added: 0006963 | |
2020-03-17 14:00 | maroneze | Status | assigned => resolved |
2020-03-17 14:00 | maroneze | Fixed in Version | => Frama-C GIT, precise the release id |
2020-03-17 14:00 | maroneze | Resolution | open => fixed |
2020-03-17 14:47 | buhler | Note Added: 0006964 | |
2020-06-12 08:59 | signoles | Fixed in Version | Frama-C GIT, precise the release id => Frama-C 21-Scandium |
2020-06-12 08:59 | signoles | Status | resolved => closed |