Frama-C Bug Tracking System - Frama-C
View Issue Details
0002298Frama-CPlug-in > wppublic2017-05-08 16:502017-05-11 15:43
Jochen 
correnson 
normalcrashalways
assignedopen 
Phosphorus-20170501-beta1xubuntu 16.04.1
 
 
0002298: "loop assigns" clause ignored in presence of "for"-prefixed clauses
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".
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 [^]
No tags attached.
c beh.c (512) 2017-05-08 16:50
https://bts.frama-c.com/file_download.php?file_id=1173&type=bug
c beh2.c (555) 2017-05-11 15:43
https://bts.frama-c.com/file_download.php?file_id=1177&type=bug
Issue History
2017-05-08 16:50JochenNew Issue
2017-05-08 16:50JochenStatusnew => assigned
2017-05-08 16:50JochenAssigned To => correnson
2017-05-08 16:50JochenFile Added: beh.c
2017-05-09 08:58virgileNote Added: 0006393
2017-05-11 15:43JochenNote Added: 0006394
2017-05-11 15:43JochenFile Added: beh2.c

Notes
(0006393)
virgile   
2017-05-09 08:58   
WP's message before the crash is misleading. In fact, when you move the for five: label below x06, the x06 loop assigns belongs to the default behavior, while x05 is associated to the `five' behavior. In the original setting, as you saw, the for five label extends to all subsequent clauses, (except for the variant, which can't be tied to a particular behavior), meaning that x05 and x06 are considered as associated to the `five' behavior and merged by the kernel before WP has a chance to see two distinct clauses. This can be seen with frama-c -print beh.c
(0006394)
Jochen   
2017-05-11 15:43   
Oops, I didn't expect "for XXX" to extend for all subsequent clauses until further notice (but "frama-c -print" confirmed it). In order to be foolproof, e.g. the 2nd item in section 2.4.1 "Assertions" of the ACSL Implementation manual could be more explicit about that.

I attach a corrected version that works fine, but shows the strange warning from issue 0002301, too; I'll mention it there.

By the way: is there a way to switch back to the anonymous behavior? If so, this should be mentioned in the manual (and if not, it should be mentioned, too).