[eacsl:typing] Update `Typing.number_ty_of_typ` to support GMP types

src/plugins/e-acsl/src/analyses/typing.ml

@@ -262,16 +262,21 @@ let coerce ~arith_operand ~ctx ~op ty =
   then { ty; op; cast = Some ctx }
   else { ty; op; cast = None }
 
-let number_ty_of_typ ty = match Cil.unrollType ty with
-  | TInt(ik, _) | TEnum({ ekind = ik }, _) -> C_integer ik
-  | TFloat(fk, _) -> C_float fk
-  | TVoid _ | TPtr _ | TArray _ | TFun _ | TComp _ | TBuiltin_va_list _ -> Nan
-  | TNamed _ -> assert false
+let number_ty_of_typ ~post ty =
+  (* Consider GMP types only in a post typing phase *)
+  if post && Gmp_types.Z.is_t ty then Gmpz
+  else if post && Gmp_types.Q.is_t ty then Rational
+  else
+    match Cil.unrollType ty with
+    | TInt(ik, _) | TEnum({ ekind = ik }, _) -> C_integer ik
+    | TFloat(fk, _) -> C_float fk
+    | TVoid _ | TPtr _ | TArray _ | TFun _ | TComp _ | TBuiltin_va_list _ -> Nan
+    | TNamed _ -> assert false
 
 let ty_of_logic_ty ?term lty =
   let get_ty = function
     | Linteger -> Gmpz
-    | Ctype ty -> number_ty_of_typ ty
+    | Ctype ty -> number_ty_of_typ ~post:false ty
     | Lreal -> Real
     | Larrow _ -> Nan
     | Ltype _ -> Error.not_yet "user-defined logic type"

src/plugins/e-acsl/src/analyses/typing.mli

@@ -79,8 +79,12 @@ val typ_of_number_ty: number_ty -> typ
     for [Gmpz], [Real.t ()] for [Real] and [TInt(ik, [[]])] for [Ctype ik].
     @raise Not_a_number in case of [Nan]. *)
 
-val number_ty_of_typ: typ -> number_ty
-(** Reverse of [typ_of_number_ty] *)
+val number_ty_of_typ: post:bool -> typ -> number_ty
+(** Reverse of [typ_of_number_ty]
+    [number_ty_of_typ ~post ty] return the {!number_ty} corresponding to a
+    C type. [post] indicates if the type is before or after the typing phase.
+    The GMP types will be recognized only in a post-typing phase.
+*)
 
 val join: number_ty -> number_ty -> number_ty
 (** {!number_ty} is a join-semi-lattice if you do not consider [Other]. If

src/plugins/e-acsl/src/code_generator/logic_functions.ml

@@ -88,7 +88,10 @@ let pred_to_block ~loc kf env ret_vi p =
 
 (* Generate the function's body for terms. *)
 let term_to_block ~loc kf env ret_ty ret_vi t =
-  Typing.type_term ~use_gmp_opt:false ~ctx:(Typing.number_ty_of_typ ret_ty) t;
+  Typing.type_term
+    ~use_gmp_opt:false
+    ~ctx:(Typing.number_ty_of_typ ~post:false ret_ty)
+    t;
   let e, env = !term_to_exp_ref kf env t in
   if Cil.isVoidType ret_ty then
     (* if the function's result is a GMP, it is the first parameter of the

src/plugins/e-acsl/src/code_generator/loops.ml

@@ -117,7 +117,7 @@ let bounds_for_small_type ~loc (t1, lv, t2) =
       let min, max = Misc.finite_min_and_max i in
       let t1 = Logic_const.tint ~loc min in
       let t2 = Logic_const.tint ~loc max in
-      let ctx = Typing.number_ty_of_typ ty in
+      let ctx = Typing.number_ty_of_typ ~post:false ty in
       (* we are assured that we will not have a GMP,
          once again because we intersected with [ity] *)
       Typing.type_term ~use_gmp_opt:false ~ctx t1;