Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002298Frama-CPlug-in > wppublic2017-05-08 16:502017-05-11 15:43
Assigned Tocorrenson 
PlatformPhosphorus-20170501-beta1OSxubuntu 16.04.1OS Version
Product Version 
Target VersionFixed in Version 
Summary0002298: "loop assigns" clause ignored in presence of "for"-prefixed clauses
DescriptionRunning "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 InformationFrama-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/", line 568, characters 30-31 Called from file "src/kernel_services/plugin_entry_points/", line 562, characters 9-16 Re-raised at file "src/kernel_services/plugin_entry_points/", line 565, characters 15-16 Called from file "src/plugins/wp/", line 855, characters 14-43 Called from file "", line 84, characters 24-34 Called from file "", line 200, characters 23-35 Called from file "", line 204, characters 12-33 Called from file "src/kernel_services/ast_data/", line 499, characters 4-187 Called from file "src/plugins/wp/", line 865, characters 4-46 Called from file "src/plugins/wp/", line 1015, characters 36-62 Called from file "", line 168, characters 20-25 Called from file "", line 168, characters 10-18 Called from file "", line 168, characters 10-18 Called from file "src/plugins/wp/", line 1023, characters 2-39 Called from file "src/plugins/wp/", line 1094, characters 15-41 Called from file "src/plugins/wp/", line 1273, characters 14-39 Called from file "src/plugins/wp/", line 1274, characters 9-22 Called from file "src/plugins/wp/", line 1363, characters 2-47 Called from file "", line 168, characters 20-25 Called from file "src/plugins/wp/", line 136, characters 4-39 Called from file "src/plugins/wp/", line 654, characters 15-40 Called from file "src/libraries/stdlib/", line 299, characters 14-17 Re-raised at file "src/libraries/stdlib/", line 299, characters 47-48 Called from file "src/libraries/stdlib/", line 300, characters 2-12 Called from file "src/libraries/stdlib/", line 300, characters 2-12 Called from file "", line 134, characters 6-20 Called from file "src/kernel_internals/runtime/", line 37, characters 4-20 Called from file "src/kernel_services/cmdline_parameters/", line 789, characters 2-9 Called from file "src/kernel_services/cmdline_parameters/", line 819, characters 18-64 Called from file "src/kernel_services/cmdline_parameters/", line 228, characters 4-8 Plug-in wp aborted: internal error. Please report as 'crash' at 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:
TagsNo tags attached.
Attached Filesc file icon beh.c [^] (512 bytes) 2017-05-08 16:50 [Show Content]
c file icon beh2.c [^] (555 bytes) 2017-05-11 15:43 [Show Content]

- Relationships

-  Notes
virgile (developer)
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
Jochen (reporter)
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 #2301, 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).

- Issue History
Date Modified Username Field Change
2017-05-08 16:50 Jochen New Issue
2017-05-08 16:50 Jochen Status new => assigned
2017-05-08 16:50 Jochen Assigned To => correnson
2017-05-08 16:50 Jochen File Added: beh.c
2017-05-09 08:58 virgile Note Added: 0006393
2017-05-11 15:43 Jochen Note Added: 0006394
2017-05-11 15:43 Jochen File Added: beh2.c

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker