Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0002158Frama-CKernel > ACSL implementationpublic2015-09-09 18:522016-06-21 14:08
Reporterazaostro 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformUbuntu linux 14.04OSUbuntu GNU/linux OS Version14.04
Product VersionFrama-C Sodium 
Target VersionFixed in VersionFrama-C Aluminium 
Summary0002158: WP crashes on the given function
Descriptionplugin WP crushes when trying to verify a size function in the repr.c.
Steps To Reproduceframa-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
         
TagsNo tags attached.
Relationships
has duplicate 0002182assigned correnson Plug-in wp aborted: internal error, Raised at file "src/wp/register.ml", line 579 
Attached Filesc repr.c (789) 2015-09-09 18:52
https://bts.frama-c.com/file_download.php?file_id=1061&type=bug

Notes
(0006031)
azaostro   
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;
}
(0006032)
azaostro   
2015-09-14 10:11   
Hello,
Can I rise the priority? It is kinda a blocker for my project now
(0006033)
correnson   
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.
(0006034)
virgile   
2015-09-14 11:51   
ACSL type-checker does not produce correct AST in this case.
(0006162)
virgile   
2016-02-24 17:27   
Fixed in git. Will be part of next release.

Issue History
Date ModifiedUsernameFieldChange
2015-09-09 18:52azaostroNew Issue
2015-09-09 18:52azaostroStatusnew => assigned
2015-09-09 18:52azaostroAssigned To => correnson
2015-09-09 18:52azaostroFile Added: repr.c
2015-09-09 23:31yakobowskiSummaryWP crushes on the given function => WP crashes on the given function
2015-09-10 11:50azaostroNote Added: 0006031
2015-09-14 10:11azaostroNote Added: 0006032
2015-09-14 10:44corrensonNote Added: 0006033
2015-09-14 11:02corrensonNote Edited: 0006033bug_revision_view_page.php?bugnote_id=6033#r229
2015-09-14 11:51virgileNote Added: 0006034
2015-09-14 11:51virgileAssigned Tocorrenson => virgile
2015-09-14 11:51virgileCategoryPlug-in > wp => Kernel > ACSL implementation
2015-10-27 23:25yakobowskiRelationship addedhas duplicate 0002182
2016-02-24 14:19virgileSource_changeset_attached => framac master 5781bddb
2016-02-24 17:27virgileNote Added: 0006162
2016-02-24 17:27virgileStatusassigned => resolved
2016-02-24 17:27virgileFixed in Version => Frama-C Aluminium
2016-02-24 17:27virgileResolutionopen => fixed
2016-06-21 14:08signolesStatusresolved => closed