0000859: ACSL pretty-printer - Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000859

Frama-C

Kernel > ACSL implementation

public

2011-06-09 15:21

2014-02-12 16:59

Reporter

ckunz

Assigned To

virgile

Priority

normal

Severity

tweak

Reproducibility

always

Status

closed

Resolution

fixed

Product Version

Frama-C Carbon-20110201

Target Version

Fixed in Version

Frama-C Nitrogen-20111001

Summary

0000859: ACSL pretty-printer

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

Tags

No tags attached.

Attached Files

Relationships

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.

Notes

Date Modified	Username	Field	Change
Issue History
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
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
2013-12-19 01:12		Source_changeset_attached	=> framac master e0bfca76
2014-02-12 16:54		Source_changeset_attached	=> framac stable/neon e0bfca76
2014-02-12 16:59		Note Added: 0004770
2014-02-12 16:59		Status	closed => resolved

Issue History