"loop assigns" clause ignored in presence of "for"-prefixed clauses
ID0002298: This issue was created automatically from Mantis Issue 2298. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002298 | Frama-C | Plug-in > wp | public | 2017-05-08 | 2017-05-11 |
| Reporter | Jochen | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | crash | Reproducibility | always |
| Platform | Phosphorus-20170501-beta1 | OS | xubuntu 16.04.1 | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
Running "frama-c -wp beh.c" on the attached program fails to prove ensures clause "x01" and assertion "x10". When the two clauses prefixed by "for five" are removed from the loop invariant, everything is proven (except ensures clause "x02", which is about behavior "five").
Apparently, the two "for five" clauses (in fact, the first of them alone does) make Frama-c ignore the following "loop assigns x06" clause.
If the two "for five" clauses are moved below the "loop assigns x06" clause, an internal error is raised (output see "Additional information" below). For this reason, I set the Severity to "crash".
Additional Information :
Frama-C's output for the internal error:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing beh.c (with preprocessing) [wp] failure: At most one loop assigns can be associated to a behavior [kernel] Current source was: beh.c:11 The full backtrace is: Raised at file "src/kernel_services/plugin_entry_points/log.ml", line 568, characters 30-31 Called from file "src/kernel_services/plugin_entry_points/log.ml", line 562, characters 9-16 Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 565, characters 15-16 Called from file "src/plugins/wp/wpAnnot.ml", line 855, characters 14-43 Called from file "list.ml", line 84, characters 24-34 Called from file "hashtbl.ml", line 200, characters 23-35 Called from file "hashtbl.ml", line 204, characters 12-33 Called from file "src/kernel_services/ast_data/annotations.ml", line 499, characters 4-187 Called from file "src/plugins/wp/wpAnnot.ml", line 865, characters 4-46 Called from file "src/plugins/wp/wpAnnot.ml", line 1015, characters 36-62 Called from file "map.ml", line 168, characters 20-25 Called from file "map.ml", line 168, characters 10-18 Called from file "map.ml", line 168, characters 10-18 Called from file "src/plugins/wp/wpAnnot.ml", line 1023, characters 2-39 Called from file "src/plugins/wp/wpAnnot.ml", line 1094, characters 15-41 Called from file "src/plugins/wp/wpAnnot.ml", line 1273, characters 14-39 Called from file "src/plugins/wp/wpAnnot.ml", line 1274, characters 9-22 Called from file "src/plugins/wp/wpAnnot.ml", line 1363, characters 2-47 Called from file "map.ml", line 168, characters 20-25 Called from file "src/plugins/wp/Generator.ml", line 136, characters 4-39 Called from file "src/plugins/wp/register.ml", line 654, characters 15-40 Called from file "src/libraries/stdlib/extlib.ml", line 299, characters 14-17 Re-raised at file "src/libraries/stdlib/extlib.ml", line 299, characters 47-48 Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12 Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Phosphorus-20170501-beta1.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines