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 "@[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
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 - 2019 MantisBT Team
Powered by Mantis Bugtracker