[e-acsl] define Analyses_datatype.Profile.pretty

Hitherto this function was defined as Datatype.undefined leading to
an exception in Translate_terms.to_exp with -e-acsl-verbose 4 because of
the call to Profile.pretty that takes place.

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

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 =