Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000859Frama-CKernel > ACSL implementationpublic2011-06-09 15:212014-02-12 16:59
Reporterckunz 
Assigned Tovirgile 
PrioritynormalSeveritytweakReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000859: ACSL pretty-printer
DescriptionInductive predicates are not printed correctly:

predicates of the form:

  inductive .... ( ... ) {
    case ...;
    case ...;
  }

are printed as:

  predicate .... ( ... ) {
    case ...;
    case ...;
  }

Additional InformationA quick fix consists of modifying cil/src/cil.ml as follows:

*** 5676,5682 ****
                 fprintf fmt "@[<hov 2>logic %a"
                   (self#pLogic_type None) rt
             | None ->
! fprintf fmt "@[<hov 2>predicate"
         end;
         fprintf fmt " %a%a%a%a"
           self#pLogic_var li.l_var_info
--- 5676,5688 ----
                 fprintf fmt "@[<hov 2>logic %a"
                   (self#pLogic_type None) rt
             | None ->
! begin
! match li.l_body with
! | LBinductive _ ->
! fprintf fmt "@[<hov 2>inductive"
! | _ ->
! fprintf fmt "@[<hov 2>predicate"
! end
         end;
         fprintf fmt " %a%a%a%a"
           self#pLogic_var li.l_var_info
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0001992)
virgile (developer)
2011-06-22 17:30

Thanks for the patch. It is applied in the current dev. version
(0004770)

2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-06-09 15:21 ckunz New Issue
2011-06-09 15:21 ckunz Status new => assigned
2011-06-09 15:21 ckunz Assigned To => virgile
2011-06-22 17:30 virgile Note Added: 0001992
2011-06-22 17:30 svn Checkin
2011-06-22 17:30 svn Status assigned => resolved
2011-06-22 17:30 svn Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2014-02-12 16:59 Note Added: 0004770
2014-02-12 16:59 Status closed => resolved


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker