Frama-C Bug Tracking System - Frama-C
View Issue Details
0000859Frama-CKernel > ACSL implementationpublic2011-06-09 15:212014-02-12 16:59
ckunz 
virgile 
normaltweakalways
closedfixed 
Frama-C Carbon-20110201 
Frama-C Nitrogen-20111001 
0000859: ACSL pretty-printer
Inductive predicates are not printed correctly: predicates of the form: inductive .... ( ... ) { case ...; case ...; } are printed as: predicate .... ( ... ) { case ...; case ...; }
A quick fix consists of modifying cil/src/cil.ml as follows: *** 5676,5682 **** fprintf fmt "@[logic %a" (self#pLogic_type None) rt | None -> ! fprintf fmt "@[predicate" end; fprintf fmt " %a%a%a%a" self#pLogic_var li.l_var_info --- 5676,5688 ---- fprintf fmt "@[logic %a" (self#pLogic_type None) rt | None -> ! begin ! match li.l_body with ! | LBinductive _ -> ! fprintf fmt "@[inductive" ! | _ -> ! fprintf fmt "@[predicate" ! end end; fprintf fmt " %a%a%a%a" self#pLogic_var li.l_var_info
No tags attached.
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:30svnCheckin
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
2014-02-12 16:59Note Added: 0004770
2014-02-12 16:59Statusclosed => resolved

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.