2021-02-27 10:15 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000634Frama-CPlug-in > Evapublic2014-02-12 16:55
Reporteryakobowski 
Assigned Topascal 
PrioritynoneSeveritytweakReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000634: Superfluous ';' in value analysis output
DescriptionThe pretty-printer for the Locations.Zone.t prints '; ' even after the last location, causing not so pretty outputs when the location contains a single zone.
(This case is very frequent for Lmap_bitwise obtained outputs.) The attached patch corrects this.
Additional InformationWill require to update our various manuals after being applied.
TagsNo tags attached.
Attached Files
  • diff file icon patch-pretty-locations.diff (1,410 bytes) 2010-12-03 13:51 -
    Index: src/memory_state/locations.ml
    ===================================================================
    --- src/memory_state/locations.ml	(révision 10740)
    +++ src/memory_state/locations.ml	(copie de travail)
    @@ -279,13 +279,15 @@
     	  Top_Param.pretty s
     	  Origin.pretty a
         | Map _ when equal m bottom ->
    -	Format.fprintf fmt "\\nothing@ "
    +	Format.fprintf fmt "\\nothing"
         | Map off ->
    -	let print_binding k v =
    -	  Format.fprintf fmt "@[<h>%a%a;@,@]@ " Base.pretty k
    +	let print_binding fmt (k, v) =
    +	  Format.fprintf fmt "@[<h>%a%a@]"
    +            Base.pretty k
                 (Int_Intervals.pretty_typ (Base.typeof k)) v
     	in
    -	(M.iter print_binding) off
    +        Pretty_utils.pp_iter ~pre:"" ~suf:"" ~sep:";@,@ "
    +	  (fun f -> M.iter (fun k v -> f (k, v))) print_binding fmt off
     (*
       let pretty_caml fmt m =
         match m with
    Index: src/memory_state/offsetmap_bitwise.ml
    ===================================================================
    --- src/memory_state/offsetmap_bitwise.ml	(révision 10740)
    +++ src/memory_state/offsetmap_bitwise.ml	(copie de travail)
    @@ -94,7 +94,7 @@
     			  ~start:bi ~stop:ei fmt)
               in
     	  if !first then first := false else Format.fprintf fmt "@," ;
    -          Format.fprintf fmt "@[%a FROM @[%a@](and default:%b)@]"
    +          Format.fprintf fmt "@[%a FROM @[%a@] (and default:%b)@]"
     	    pp_left typ V.pretty v default
     	in
     	Format.fprintf fmt "@[<v>";
    
    diff file icon patch-pretty-locations.diff (1,410 bytes) 2010-12-03 13:51 +

-Relationships
+Relationships

-Notes
There are no notes attached to this issue.
+Notes

-Issue History
Date Modified Username Field Change
2010-12-03 13:51 yakobowski New Issue
2010-12-03 13:51 yakobowski Status new => assigned
2010-12-03 13:51 yakobowski Assigned To => pascal
2010-12-03 13:51 yakobowski File Added: patch-pretty-locations.diff
2010-12-03 15:55 svn
2010-12-03 15:55 svn Status assigned => resolved
2010-12-03 15:55 svn Resolution open => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:35 signoles Status resolved => closed
2013-12-19 01:12 yakobowski Source_changeset_attached => framac master 045561c8
2014-02-12 16:55 yakobowski Source_changeset_attached => framac stable/neon 045561c8
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History