Frama-C Bug Tracking System - Frama-C
View Issue Details
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

Notes
(0001992)
virgile   
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
2011-06-09 15:21ckunzNew Issue
2011-06-09 15:21ckunzStatusnew => assigned
2011-06-09 15:21ckunzAssigned To => virgile
2011-06-22 17:30virgileNote Added: 0001992
2011-06-22 17:30svn
2011-06-22 17:30svnStatusassigned => resolved
2011-06-22 17:30svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2013-12-19 01:12Source_changeset_attached => framac master e0bfca76
2014-02-12 16:54Source_changeset_attached => framac stable/neon e0bfca76
2014-02-12 16:59Note Added: 0004770
2014-02-12 16:59Statusclosed => resolved