diff --git a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml index d0cc26dfed7508044bf2480bbf7231754002dc10..f96c0a09eb38d5eadd73810282da2b7d1660cdae 100644 --- a/src/plugins/e-acsl/src/analyses/analyses_datatype.ml +++ b/src/plugins/e-acsl/src/analyses/analyses_datatype.ml @@ -337,6 +337,16 @@ struct let structural_descr = Structural_descr.t_abstract let rehash = Datatype.identity let name = "E-ACSL.Profile" + let pretty fmt m = + let first = ref true in + let pp_vi v i = + if !first + then first := false + else Format.fprintf fmt " "; + Format.fprintf fmt "%a:%a" + Logic_var.pretty v Analyses_types.pp_ival i + in + Logic_var.Map.iter pp_vi m end) let is_empty = Logic_var.Map.is_empty diff --git a/src/plugins/e-acsl/src/analyses/analyses_types.ml b/src/plugins/e-acsl/src/analyses/analyses_types.ml index 67632c2c116db506d5aa14363f0ddaf6ffda112c..a5a1f12468a7698020d8a3eeb74511df9d7c4b9f 100644 --- a/src/plugins/e-acsl/src/analyses/analyses_types.ml +++ b/src/plugins/e-acsl/src/analyses/analyses_types.ml @@ -76,6 +76,13 @@ type ival = | Real | Nan +let pp_ival fmt = function + | Ival i -> Ival.pretty fmt i + | Float _ -> Format.fprintf fmt "F" + | Rational -> Format.fprintf fmt "Q" + | Real -> Format.fprintf fmt "R" + | Nan -> Format.fprintf fmt "Nan" + (** Type of types inferred by the type inference for types representing numbers *) type number_ty =