rename real.ml to rational.ml and prune its API

src/plugins/e-acsl/Makefile.in

@@ -87,7 +87,7 @@ SRC_CODE_GENERATOR:= \
 	gmp \
 	label \
 	env \
-	real \
+	rational \
 	loops \
 	quantif \
 	at_with_lscope \

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

@@ -304,7 +304,9 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
     let vi_of_lv, exp_of_lv, env = Env.Logic_binding.add ~ty env lv in
     let e, env = term_to_exp kf env t in
     let ty = Cil.typeOf e in
-    let init_set = if Real.is_t ty then Real.init_set else Gmp.init_set in
+    let init_set =
+      if Gmp_types.Q.is_t ty then Rational.init_set else Gmp.init_set
+    in
     let let_stmt = init_set ~loc (Cil.var vi_of_lv) exp_of_lv  e in
     let stmts, env =
       mk_nested_loops ~loc mk_innermost_block kf env lscope_vars'
@@ -320,9 +322,8 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
     Error.not_yet
       "creating nested loops from global logic variable"
 
-
 (*
 Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
 End:
 *)

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

@@ -70,6 +70,6 @@ val term_to_exp_ref:
 
 (*
 Local Variables:
-compile-command: "make"
+compile-command: "make -C ../.."
 End:
 *)

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

@@ -22,15 +22,6 @@
 
 open Cil_types
 
-let t () =
-  (* When support for irrationals will be provided,
-    the following typ MUST be changed into a typ that can represent them.
-    It is sound to use GMPQ for the time being since irrationals
-    raise not_yet. *)
-  Gmp_types.Q.t ()
-
-let is_t ty = Cil_datatype.Typ.equal ty (t ())
-
 (* No init_set for GMPQ: init then set separately *)
 let init_set ~loc lval vi_e e =
   Cil.mkStmt
@@ -39,12 +30,15 @@ let init_set ~loc lval vi_e e =
       [ Gmp.init ~loc vi_e ;
         Gmp.affect ~loc lval vi_e e ]))
 
-let mk_real ~loc ?name e env t_opt =
-  if Gmp_types.Z.is_t (Cil.typeOf e) then
+let create ~loc ?name e env 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
+    e, env
   else
     let _, e, env =
       Env.new_var
@@ -52,7 +46,7 @@ let mk_real ~loc ?name e env t_opt =
         ?name
         env
         t_opt
-        (t ())
+        (Gmp_types.Q.t ())
         (fun vi vi_e ->
            [ Gmp.init ~loc vi_e ;
              Gmp.affect ~loc (Cil.var vi) vi_e e ])
@@ -141,14 +135,14 @@ let normalize_str str =
     Error.not_yet "number not written in decimal expansion"
 
 let cast_to_z ~loc:_ ?name:_ e _env =
-  assert (is_t (Cil.typeOf e));
+  assert (Gmp_types.Q.is_t (Cil.typeOf e));
   Error.not_yet "reals: cast from R to Z"
 
 let add_cast ~loc ?name e env ty =
   (* TODO: The best solution would actually be to directly write all the needed
      functions as C builtins then just call them here depending on the situation
      at hand. *)
-  assert (is_t (Cil.typeOf e));
+  assert (Gmp_types.Q.is_t (Cil.typeOf e));
   let get_double e env =
     let _, e, env =
       Env.new_var
@@ -188,14 +182,11 @@ let add_cast ~loc ?name e env ty =
   | _ ->
     Error.not_yet "R to <typ>"
 
-let real ~loc e env =
-  if is_t (Cil.typeOf e) then e, env else mk_real ~loc e env None
-
 let cmp ~loc bop e1 e2 env t_opt =
   let fname = "__gmpq_cmp" in
   let name = Misc.name_of_binop bop in
-  let e1, env = real ~loc e1 env in
-  let e2, env = real ~loc e2 env in
+  let e1, env = create ~loc e1 env None (* TODO: t1_opt could be provided *) in
+  let e2, env = create ~loc e2 env None (* TODO: t2_opt could be provided *) in
   let _, e, env =
     Env.new_var
       ~loc
@@ -214,7 +205,7 @@ let new_var_and_init ~loc ?scope ?name env t_opt mk_stmts =
     ?name
     env
     t_opt
-    (t ())
+    (Gmp_types.Q.t ())
     (fun v e -> Gmp.init ~loc e :: mk_stmts v e)
 
 let name_arith_bop = function
@@ -227,8 +218,8 @@ let name_arith_bop = function
 
 let binop ~loc bop e1 e2 env t_opt =
   let name = name_arith_bop bop in
-  let e1, env = real ~loc e1 env in
-  let e2, env = real ~loc e2 env in
+  let e1, env = create ~loc e1 env None (* TODO: t1_opt could be provided *) in
+  let e2, env = create ~loc e2 env None (* TODO: t2_opt could be provided *) in
   let mk_stmts _ e = [ Misc.mk_call ~loc name [ e; e1; e2 ] ] in
   let name = Misc.name_of_binop bop in
   let _, e, env = new_var_and_init ~loc ~name env t_opt mk_stmts in

src/plugins/e-acsl/src/code_generator/real.mli → src/plugins/e-acsl/src/code_generator/rational.mli

@@ -20,23 +20,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** Realary for real numbers.
-    For the sake of maintainability, the only access to the installed
-    real library MUST be through the current module.
-    For example, if it is `libgmp` then we MUST NEVER directly call gmp
-    builtins in outer modules (e.g. `Typing` or `Translate`) for handling reals.
-    This way, if we want to change `libgmp` to something else, say `mpfr`, then
-    all changes will be centralized here. *)
+(** Generation of rational numbers. *)
 
 open Cil_types
 
-val t: unit -> typ
-(** C type representing reals in the generated code  *)
-
-val is_t: typ -> bool
-(** Is the typ real? *)
-
-val mk_real: loc:location -> ?name:string -> exp -> Env.t -> term option ->
+val create: loc:location -> ?name:string -> exp -> Env.t -> term option ->
   exp * Env.t
 (** Create a real *)
 

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

@@ -84,7 +84,7 @@ let add_cast ~loc ?name env ctx strnum t_opt e =
   in
   let e, env = match strnum with
     | Str_Z -> mk_mpz e
-    | Str_R -> Real.mk_real ~loc ?name e env t_opt
+    | Str_R -> Rational.create ~loc ?name e env t_opt
     | C_number -> e, env
   in
   match ctx with
@@ -97,9 +97,9 @@ let add_cast ~loc ?name env ctx strnum t_opt e =
       (* Z --> Z *)
       e, env
     | false, true ->
-      if Real.is_t ty then
+      if Gmp_types.Q.is_t ty then
         (* R --> Z *)
-        Real.cast_to_z ~loc ?name e env
+        Rational.cast_to_z ~loc ?name e env
       else
         (* C integer --> Z *)
         let e =
@@ -114,9 +114,9 @@ let add_cast ~loc ?name env ctx strnum t_opt e =
         in
         mk_mpz e
     | _, false ->
-      if Real.is_t ctx then
-        if Real.is_t (Cil.typeOf e) then (* R --> R *) e, env
-        else (* C integer or Z --> R *) Real.mk_real ~loc ?name e env t_opt
+      if Gmp_types.Q.is_t ctx then
+        if Gmp_types.Q.is_t (Cil.typeOf e) then (* R --> R *) e, env
+        else (* C integer or Z --> R *) Rational.create ~loc ?name e env t_opt
       else if Gmp_types.Z.is_t ty || strnum = Str_Z then
         (* Z --> C type or the integer is represented by a string:
            anyway, it fits into a C integer: convert it *)
@@ -134,16 +134,16 @@ let add_cast ~loc ?name env ctx strnum t_opt e =
             (fun v _ -> [ Misc.mk_call ~loc ~result:(Cil.var v) fname [ e ] ])
         in
         e, env
-      else if Real.is_t ty || strnum = Str_R then
+      else if Gmp_types.Q.is_t ty || strnum = Str_R then
         (* R --> C type or the real is represented by a string *)
-        Real.add_cast ~loc ?name e env ctx
+        Rational.add_cast ~loc ?name e env ctx
       else
         (* C type --> another C type *)
         Cil.mkCastT ~force:false ~e ~oldt:ty ~newt:ctx, env
 
 let constant_to_exp ~loc t c =
   let mk_real s =
-    let s = Real.normalize_str s in
+    let s = Rational.normalize_str s in
     Cil.mkString ~loc s, Str_R
   in
   match c with
@@ -164,7 +164,7 @@ let constant_to_exp ~loc t c =
        | Some ty, (ILongLong | IULongLong) when Gmp_types.Z.is_t ty ->
          (* too large integer *)
          Cil.mkString ~loc (Integer.to_string n), Str_Z
-       | Some ty, _ when Real.is_t ty ->
+       | Some ty, _ when Gmp_types.Q.is_t ty ->
          mk_real (Integer.to_string n)
        | (None | Some _), _ ->
          (* do not keep the initial string representation because the generated
@@ -206,7 +206,7 @@ let conditional_to_exp ?(name="if") loc t_opt e1 (e2, env2) (e3, env3) =
           let lv = Cil.var v in
           let ty = Cil.typeOf ev in
           let init_set =
-            assert (not (Real.is_t ty));
+            assert (not (Gmp_types.Q.is_t ty));
             Gmp.init_set
           in
           let affect e = init_set ~loc lv ev e in
@@ -299,7 +299,7 @@ and context_insensitive_term_to_exp kf env t =
           (fun _ ev -> [ Misc.mk_call ~loc name [ ev; e ] ])
       in
       e, env, C_number, ""
-    else if Real.is_t ty then
+    else if Gmp_types.Q.is_t ty then
       not_yet env "reals: Neg | BNot"
     else
       Cil.new_exp ~loc (UnOp(op, e, ty)), env, C_number, ""
@@ -331,8 +331,8 @@ and context_insensitive_term_to_exp kf env t =
         Env.new_var_and_mpz_init ~loc ~name env (Some t) mk_stmts
       in
       e, env, C_number, ""
-    else if Real.is_t ty then
-      let e, env = Real.binop ~loc bop e1 e2 env (Some t) in
+    else if Gmp_types.Q.is_t ty then
+      let e, env = Rational.binop ~loc bop e1 e2 env (Some t) in
       e, env, C_number, ""
     else begin
       assert (Logic_typing.is_integral_type t.term_type);
@@ -377,8 +377,8 @@ and context_insensitive_term_to_exp kf env t =
       let name = Misc.name_of_binop bop in
       let _, e, env = Env.new_var_and_mpz_init ~loc ~name env t mk_stmts in
       e, env, C_number, ""
-    else if Real.is_t ty then
-      let e, env = Real.binop ~loc bop e1 e2 env (Some t) in
+    else if Gmp_types.Q.is_t ty then
+      let e, env = Rational.binop ~loc bop e1 e2 env (Some t) in
       e, env, C_number, ""
     else begin
       assert (Logic_typing.is_integral_type t.term_type);
@@ -611,7 +611,7 @@ and comparison_to_exp
     in
     Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
   | Typing.Rational ->
-    Real.cmp ~loc bop e1 e2 env t_opt
+    Rational.cmp ~loc bop e1 e2 env t_opt
   | Typing.Real ->
     Error.not_yet "comparison involving real numbers"
 
@@ -642,7 +642,9 @@ and at_to_exp_no_lscope env t_opt label e =
       (* either a standard C affectation or a call to an initializer according
          to the type of [e] *)
       let ty = Cil.typeOf e in
-      let init_set = if Real.is_t ty then Real.init_set else Gmp.init_set in
+      let init_set =
+        if Gmp_types.Q.is_t ty then Rational.init_set else Gmp.init_set
+      in
       let new_stmt = init_set ~loc (Cil.var res_v) res e in
       assert (!env_ref == new_env);
       (* generate the new block of code for the labeled statement and the
@@ -672,7 +674,7 @@ and env_of_li li kf env loc =
     | Typing.Gmpz ->
       Gmp.init_set ~loc (Cil.var vi) vi_e e
     | Typing.Rational ->
-      Real.init_set ~loc (Cil.var vi) vi_e e
+      Rational.init_set ~loc (Cil.var vi) vi_e e
     | Typing.Real ->
       Error.not_yet "real number"
   in