View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002158 | Frama-C | Kernel > ACSL implementation | public | 2015-09-09 18:52 | 2016-06-21 14:08 | ||||
Reporter | azaostro | ||||||||
Assigned To | virgile | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Platform | Ubuntu linux 14.04 | OS | Ubuntu GNU/linux | OS Version | 14.04 | ||||
Product Version | Frama-C Sodium | ||||||||
Target Version | Fixed in Version | Frama-C Aluminium | |||||||
Summary | 0002158: WP crashes on the given function | ||||||||
Description | plugin WP crushes when trying to verify a size function in the repr.c. | ||||||||
Steps To Reproduce | frama-c -wp repr.c -wp-fct size Raises the error: [jessie3] Loading Why3 configuration... [jessie3] Why3 environment loaded. [jessie3] Loading Why3 theories... [jessie3] Loading Why3 modules... [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing repr.c (with preprocessing) [wp] Running WP plugin... [wp] Collecting axiomatic usage [wp] warning: Missing RTE guards [wp] failure: *** Label Label 'L' not-found [kernel] Current source was: repr.c:21 The full backtrace is: Raised at file "src/kernel/log.ml", line 524, characters 30-31 Called from file "src/kernel/log.ml", line 518, characters 9-16 Re-raised at file "src/kernel/log.ml", line 521, characters 15-16 Called from file "src/wp/LogicCompiler.ml", line 754, characters 16-79 Called from file "list.ml", line 55, characters 20-23 Called from file "src/wp/LogicCompiler.ml", line 766, characters 17-61 Called from file "src/wp/LogicSemantics.ml", line 524, characters 18-44 Called from file "src/wp/Warning.ml", line 139, characters 6-10 Called from file "src/wp/LogicSemantics.ml", line 802, characters 12-32 Called from file "src/wp/Context.ml", line 31, characters 12-17 Re-raised at file "src/wp/Context.ml", line 34, characters 41-46 Called from file "src/wp/LogicCompiler.ml", line 367, characters 20-35 Called from file "src/wp/Warning.ml", line 139, characters 6-10 Called from file "src/wp/LogicSemantics.ml", line 802, characters 12-32 Called from file "src/wp/Context.ml", line 31, characters 12-17 Re-raised at file "src/wp/Context.ml", line 34, characters 41-46 Called from file "src/wp/LogicCompiler.ml", line 367, characters 20-35 Called from file "src/wp/LogicSemantics.ml", line 545, characters 16-33 Called from file "src/wp/Warning.ml", line 139, characters 6-10 Called from file "src/wp/LogicSemantics.ml", line 802, characters 12-32 Called from file "src/wp/Context.ml", line 31, characters 12-17 Re-raised at file "src/wp/Context.ml", line 34, characters 41-46 Called from file "src/wp/LogicCompiler.ml", line 367, characters 20-35 Called from file "src/wp/LogicSemantics.ml", line 546, characters 16-33 Called from file "src/wp/Warning.ml", line 139, characters 6-10 Called from file "src/wp/LogicSemantics.ml", line 802, characters 12-32 Called from file "src/wp/Context.ml", line 31, characters 12-17 Re-raised at file "src/wp/Context.ml", line 34, characters 41-46 Called from file "src/wp/Warning.ml", line 139, characters 6-10 Called from file "src/wp/LogicSemantics.ml", line 802, characters 12-32 Called from file "src/wp/Context.ml", line 31, characters 12-17 Re-raised at file "src/wp/Context.ml", line 34, characters 41-46 Called from file "src/wp/LogicCompiler.ml", line 367, characters 20-35 Called from file "src/wp/LogicCompiler.ml", line 335, characters 21-32 Called from file "src/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/wp/Context.ml", line 69, characters 43-48 Called from file "src/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/wp/Context.ml", line 69, characters 43-48 Called from file "src/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/wp/Context.ml", line 69, characters 43-48 Called from file "src/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/wp/Context.ml", line 69, characters 43-48 Called from file "src/wp/LogicCompiler.ml", line 564, characters 21-54 Called from file "src/wp/Model.ml", line 232, characters 14-17 Called from file "src/wp/LogicCompiler.ml", line 763, characters 10-23 Called from file "src/wp/LogicSemantics.ml", line 524, characters 18-44 Called from file "src/wp/Warning.ml", line 139, characters 6-10 Called from file "src/wp/LogicSemantics.ml", line 802, characters 12-32 Called from file "src/wp/Context.ml", line 31, characters 12-17 Re-raised at file "src/wp/Context.ml", line 34, characters 41-46 Called from file "src/wp/LogicCompiler.ml", line 367, characters 20-35 Called from file "src/wp/LogicSemantics.ml", line 338, characters 36-55 Called from file "src/wp/Warning.ml", line 139, characters 6-10 Called from file "src/wp/LogicSemantics.ml", line 813, characters 12-42 Called from file "src/wp/Context.ml", line 31, characters 12-17 Re-raised at file "src/wp/Context.ml", line 34, characters 41-46 Called from file "src/wp/Warning.ml", line 155, characters 14-18 Called from file "src/wp/cfgWP.ml", line 462, characters 23-140 Called from file "src/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/wp/Context.ml", line 69, characters 43-48 Called from file "src/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/wp/Context.ml", line 69, characters 43-48 Called from file "src/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/wp/Context.ml", line 69, characters 43-48 Called from file "src/wp/Context.ml", line 68, characters 14-17 Re-raised at file "src/wp/Context.ml", line 69, characters 43-48 Called from file "list.ml", line 84, characters 24-34 Called from file "src/wp/calculus.ml", line 331, characters 22-64 Called from file "src/wp/calculus.ml", line 341, characters 23-45 Called from file "src/wp/calculus.ml", line 586, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 589, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 586, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 602, characters 10-33 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 586, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 589, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 583, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 598, characters 22-40 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 589, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 583, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 602, characters 10-33 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 586, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 583, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 598, characters 22-40 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 583, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 396, characters 20-39 Called from file "src/wp/calculus.ml", line 610, characters 10-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 589, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 583, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 589, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 579, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 574, characters 20-43 Called from file "src/wp/calculus.ml", line 536, characters 19-40 Called from file "src/wp/calculus.ml", line 724, characters 40-59 Called from file "set.ml", line 304, characters 38-41 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 "map.ml", line 168, characters 10-18 Called from file "map.ml", line 168, characters 10-18 Called from file "src/wp/calculus.ml", line 724, characters 4-64 Called from file "src/wp/calculus.ml", line 770, characters 19-51 Called from file "src/wp/cfgWP.ml", line 1402, characters 39-62 Called from file "src/wp/cfgWP.ml", line 1391, characters 14-837 Called from file "src/wp/Model.ml", line 111, characters 17-20 Re-raised at file "src/wp/Model.ml", line 116, characters 25-28 Called from file "src/wp/Model.ml", line 117, characters 19-36 Called from file "src/wp/register.ml", line 451, characters 20-31 Called from file "src/wp/register.ml", line 574, characters 17-24 Re-raised at file "src/wp/register.ml", line 578, characters 27-29 Called from file "src/wp/register.ml", line 575, characters 17-24 Re-raised at file "src/wp/register.ml", line 579, characters 30-32 Called from file "src/wp/register.ml", line 575, characters 17-24 Re-raised at file "src/wp/register.ml", line 579, characters 30-32 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 37, characters 4-20 Called from file "src/kernel/cmdline.ml", line 763, characters 2-9 Called from file "src/kernel/cmdline.ml", line 216, characters 4-8 | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
||||||
|
![]() |
|
azaostro (reporter) 2015-09-10 11:50 |
I discovered that it is the size_rec logic function which is problematic for WP. Here is a smaller example: /*@ logic integer size_rec(int* busybits, integer capa) = @ (capa <= 0) ? 0 : @ (busybits[capa-1] != 0) ? 1 + size_rec(busybits, capa - 1) : @ size_rec(busybits, capa - 1); */ /*@ ensures \result == size_rec(busybits, 0); */ int size(int busybits[0]) { return 0; } |
azaostro (reporter) 2015-09-14 10:11 |
Hello, Can I rise the priority? It is kinda a blocker for my project now |
correnson (manager) 2015-09-14 10:44 Last edited: 2015-09-14 11:02 |
This is an internal normalization problem. Workaround: make the implicit label parameter of size_rec explicit: /*@ logic integer size_rec{L}(int* busybits, integer capa) = @ (capa <= 0) ? 0 : @ (busybits[capa-1] != 0) ? 1 + size_rec(busybits, capa - 1) : @ size_rec(busybits, capa - 1); */ EDIT: the label is only required at declaration. The recursive calls are implicitly at {L} and this is correctly normalized. |
virgile (developer) 2015-09-14 11:51 |
ACSL type-checker does not produce correct AST in this case. |
virgile (developer) 2016-02-24 17:27 |
Fixed in git. Will be part of next release. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2015-09-09 18:52 | azaostro | New Issue | |
2015-09-09 18:52 | azaostro | Status | new => assigned |
2015-09-09 18:52 | azaostro | Assigned To | => correnson |
2015-09-09 18:52 | azaostro | File Added: repr.c | |
2015-09-09 23:31 | yakobowski | Summary | WP crushes on the given function => WP crashes on the given function |
2015-09-10 11:50 | azaostro | Note Added: 0006031 | |
2015-09-14 10:11 | azaostro | Note Added: 0006032 | |
2015-09-14 10:44 | correnson | Note Added: 0006033 | |
2015-09-14 11:02 | correnson | Note Edited: 0006033 | View Revisions |
2015-09-14 11:51 | virgile | Note Added: 0006034 | |
2015-09-14 11:51 | virgile | Assigned To | correnson => virgile |
2015-09-14 11:51 | virgile | Category | Plug-in > wp => Kernel > ACSL implementation |
2015-10-27 23:25 | yakobowski | Relationship added | has duplicate 0002182 |
2016-02-24 14:19 | virgile | Source_changeset_attached | => framac master 5781bddb |
2016-02-24 17:27 | virgile | Note Added: 0006162 | |
2016-02-24 17:27 | virgile | Status | assigned => resolved |
2016-02-24 17:27 | virgile | Fixed in Version | => Frama-C Aluminium |
2016-02-24 17:27 | virgile | Resolution | open => fixed |
2016-06-21 14:08 | signoles | Status | resolved => closed |