[eacsl:codegen] Add support to create GMP rational from GMP integer

src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h

@@ -154,6 +154,12 @@ extern void __gmpq_set_ui(mpq_t q, unsigned long int n, unsigned long int d)
 extern void __gmpq_set_si(mpq_t q, signed long int n, unsigned long int d)
   __attribute__((FC_BUILTIN));
 
+/*@ requires \valid_read(z_orig);
+  @ requires \valid(q);
+  @ assigns *q \from *z_orig; */
+extern void __gmpq_set_z(mpq_t q, const mpz_t z_orig)
+  __attribute__((FC_BUILTIN));
+
 /*@ allocates q;
   @ ensures \valid(q);
   @ ensures \initialized(q);
@@ -173,6 +179,12 @@ extern void __gmpz_set_ui(mpz_t z, unsigned long int n)
 extern void __gmpz_set_si(mpz_t z, signed long int n)
   __attribute__((FC_BUILTIN));
 
+/*@ requires \valid_read(q_orig);
+  @ requires \valid(z);
+  @ assigns *z \from *q_orig; */
+extern void __gmpz_set_q(mpz_t z, const mpq_t q_orig)
+  __attribute__((FC_BUILTIN));
+
 /*************/
 /* Finalizer */
 /*************/

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

@@ -42,38 +42,49 @@ exception Longlong of ikind
 
 let get_set_suffix_and_arg res_ty e =
   let ty = Cil.typeOf e in
-  if Gmp_types.Z.is_t ty || Gmp_types.Q.is_t ty then "", [ e ]
-  else
-    let args_uisi e =
-      if Gmp_types.Z.is_t res_ty then [ e ]
-      else begin
-        assert (Gmp_types.Q.is_t res_ty);
-        [ e; Cil.one ~loc:e.eloc ]
-      end
-    in
-    match Cil.unrollType ty with
-    | TInt(IChar, _) ->
-      (if Cil.theMachine.Cil.theMachine.char_is_unsigned then "_ui"
-       else "_si"),
-      args_uisi e
-    | TInt((IBool | IUChar | IUInt | IUShort | IULong), _) ->
-      "_ui", args_uisi e
-    | TInt((ISChar | IShort | IInt | ILong), _) -> "_si", args_uisi e
-    | TInt((ILongLong | IULongLong as ikind), _) -> raise (Longlong ikind)
-    | TPtr(TInt(IChar, _), _) ->
-      "_str",
-      (* decimal base for the number given as string *)
-      [ e; Cil.integer ~loc:e.eloc 10 ]
-    | TFloat((FDouble | FFloat), _) ->
-      (* FFloat is a strict subset of FDouble (modulo exceptional numbers)
-         Hence, calling [set_d] for both of them is sound.
-         HOWEVER: the machdep MUST NOT be vulnerable to double rounding
-         [TODO] check the statement above *)
-      "_d", [ e ]
-    | TFloat(FLongDouble, _) ->
-      Error.not_yet "creating gmp from long double"
-    | _ ->
-      assert false
+  let exp_number_ty = Typing.number_ty_of_typ ~post:true ty in
+  let res_number_ty = Typing.number_ty_of_typ ~post:true res_ty in
+  let args_uisi e =
+    if Gmp_types.Z.is_t res_ty then [ e ]
+    else begin
+      assert (Gmp_types.Q.is_t res_ty);
+      [ e; Cil.one ~loc:e.eloc ]
+    end
+  in
+  match (exp_number_ty, res_number_ty) with
+  | Typing.Gmpz, Typing.Gmpz | Typing.Rational, Typing.Rational ->
+    "", [ e ]
+  | Typing.Gmpz, Typing.Rational ->
+    "_z", [ e ]
+  | Typing.Rational, Typing.Gmpz ->
+    "_q", [ e ]
+  | Typing.C_integer IChar, _ ->
+    (if Cil.theMachine.Cil.theMachine.char_is_unsigned then "_ui"
+     else "_si"),
+    args_uisi e
+  | Typing.C_integer (IBool | IUChar | IUInt | IUShort | IULong), _ ->
+    "_ui", args_uisi e
+  | Typing.C_integer (ISChar | IShort | IInt | ILong), _ ->
+    "_si", args_uisi e
+  | Typing.C_integer (ILongLong | IULongLong as ikind), _ ->
+    raise (Longlong ikind)
+  | Typing.C_float (FDouble | FFloat), _ ->
+    (* FFloat is a strict subset of FDouble (modulo exceptional numbers)
+       Hence, calling [set_d] for both of them is sound.
+       HOWEVER: the machdep MUST NOT be vulnerable to double rounding
+       [TODO] check the statement above *)
+    "_d", [ e ]
+  | Typing.C_float FLongDouble, _ ->
+    Error.not_yet "creating gmp from long double"
+  | Typing.Gmpz, _ | Typing.Rational, _ | Typing.Real, _ | Typing.Nan, _ -> (
+      match Cil.unrollType ty with
+      | TPtr(TInt(IChar, _), _) ->
+        "_str",
+        (* decimal base for the number given as string *)
+        [ e; Cil.integer ~loc:e.eloc 10 ]
+      | _ ->
+        assert false
+    )
 
 let generic_affect ~loc fname lv ev e =
   let ty = Cil.typeOf ev in

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

@@ -32,12 +32,7 @@ let init_set ~loc lval vi_e e =
 
 let create ~loc ?name e env kf t_opt =
   let ty = Cil.typeOf e in
-  if Gmp_types.Z.is_t ty then
-    (* GMPQ has no builtin for creating Q from Z. Hence:
-       1) Get the MPZ as a string: gmZ_get_str
-       2) Set the MPQ with that string: gmpQ_set_str *)
-    Error.not_yet "reals: creating Q from Z"
-  else if Gmp_types.Q.is_t ty then
+  if Gmp_types.Q.is_t ty then
     e, env
   else
     let _, e, env =