ACSL pretty-printer

ID0000859: This issue was created automatically from Mantis Issue 859. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000859	Frama-C	Kernel > ACSL implementation	public	2011-06-09	2014-02-12

Reporter	ckunz	Assigned To	virgile	Resolution	fixed
Priority	normal	Severity	tweak	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Carbon-20110201	Target Version	-	Fixed in Version	Frama-C Nitrogen-20111001

Description :

Inductive predicates are not printed correctly:

predicates of the form:

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

are printed as:

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

Additional Information :

A 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