Merge branch 'bugfix/kostyantyn/mpz-rename' into 'master'

Renamed mpz module to gmpz to avoid link-time clashes with apron module (see issue #17 )



See merge request !46

src/plugins/e-acsl/Makefile.in

@@ -54,7 +54,7 @@ PLUGIN_CMO:= local_config \
 	rte \
 	error \
 	misc \
-	mpz \
+	gmpz \
 	literal_strings \
 	mmodel_analysis \
 	dup_functions \

src/plugins/e-acsl/env.ml

@@ -170,8 +170,8 @@ let acc_list_rev acc l = List.fold_left (fun acc x -> x :: acc) acc l
 let do_new_var ~loc init ?(scope=Local_block) ?(name="") env t ty mk_stmts =
   let local_env, tl_env = top init env in
   let local_block = local_env.block_info in
-  let is_t = Mpz.is_t ty in
-  if is_t then Mpz.is_now_referenced ();
+  let is_t = Gmpz.is_t ty in
+  if is_t then Gmpz.is_now_referenced ();
   let n = succ env.cpt in
   let v =
     Cil.makeVarinfo
@@ -203,7 +203,7 @@ let do_new_var ~loc init ?(scope=Local_block) ?(name="") env t ty mk_stmts =
 (*      Options.feedback "memoizing %a for term %a" 
 	Varinfo.pretty v (fun fmt t -> match t with None -> Format.fprintf fmt
 	  "NONE" | Some t -> Term.pretty fmt t) t;*)
-      { clear_stmts = Mpz.clear ~loc e :: tbl.clear_stmts;
+      { clear_stmts = Gmpz.clear ~loc e :: tbl.clear_stmts;
 	new_exps = match t with
 	| None -> tbl.new_exps
 	| Some t -> Term.Map.add t (v, e) tbl.new_exps }
@@ -263,8 +263,8 @@ let new_var ~loc ?(init=false) ?(scope=Local_block) ?name env t ty mk_stmts =
 
 let new_var_and_mpz_init ~loc ?init ?scope ?name env t mk_stmts =
   new_var 
-    ~loc ?init ?scope ?name env t (Mpz.t ()) 
-    (fun v e -> Mpz.init ~loc e :: mk_stmts v e)
+    ~loc ?init ?scope ?name env t (Gmpz.t ()) 
+    (fun v e -> Gmpz.init ~loc e :: mk_stmts v e)
 
 module Logic_binding = struct
 
@@ -273,7 +273,7 @@ module Logic_binding = struct
       | Some ty -> ty
       | None -> match logic_v.lv_type with
 	| Ctype ty -> ty
-	| Linteger -> Mpz.t ()
+	| Linteger -> Gmpz.t ()
 	| Ltype _ as ty when Logic_const.is_boolean_type ty -> Cil.charType
 	| Ltype _ | Lvar _ | Lreal | Larrow _ as lty -> 
 	  let msg = 

src/plugins/e-acsl/main.ml

@@ -152,7 +152,7 @@ let generate_code =
 	    Project.on
 	      dup_prj
 	      (fun () ->
-                Mpz.init_t ();
+                Gmpz.init_t ();
                 Mmodel_analysis.reset ();
 		let visit prj = Visit.do_visit ~prj true in
 		let prj = File.create_project_from_visitor name visit in
@@ -242,7 +242,7 @@ let main () =
     if Options.Check.get () then
       apply_on_e_acsl_ast
         (fun () ->
-          Mpz.init_t ();
+          Gmpz.init_t ();
           ignore (check ()))
         ()
 

src/plugins/e-acsl/quantif.ml

@@ -191,10 +191,10 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
       let var_x, x, env = Env.Logic_binding.add ~ty env logic_x in
       let lv_x = var var_x in
       let env = 
-	if Mpz.is_t ty then Env.add_stmt env (Mpz.init ~loc x) else env 
+	if Gmpz.is_t ty then Env.add_stmt env (Gmpz.init ~loc x) else env 
       in
       let llv = cvar_to_lvar var_x in
-      if not (Mpz.is_t ty) then Typing.unsafe_unify ~from:logic_x llv;
+      if not (Gmpz.is_t ty) then Typing.unsafe_unify ~from:logic_x llv;
       (* build the inner loops and loop body *)
       let body, env = mk_for_loop env tl in
       (* initialize the loop counter to [t1] *)
@@ -202,7 +202,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
       let init_blk, env = 
 	Env.pop_and_get 
 	  env
-	  (Mpz.affect ~loc:e1.eloc lv_x x e1)
+	  (Gmpz.affect ~loc:e1.eloc lv_x x e1)
 	  ~global_clear:false
 	  Env.Middle
       in
@@ -233,7 +233,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
       let next_blk, env = 
 	Env.pop_and_get
 	  env
-	  (Mpz.affect ~loc:incr.eloc lv_x x incr)
+	  (Gmpz.affect ~loc:incr.eloc lv_x x incr)
 	  ~global_clear:false
 	  Env.Middle
       in

src/plugins/e-acsl/translate.ml

@@ -118,7 +118,7 @@ let conditional_to_exp ?(name="if") loc ctx e1 (e2, env2) (e3, env3) =
 	ctx
 	(fun v ev ->
 	  let lv = Cil.var v in
-	  let affect e = Mpz.init_set ~loc lv ev e in
+	  let affect e = Gmpz.init_set ~loc lv ev e in
 	  let then_block, _ = 
 	    let s = affect e2 in
 	    Env.pop_and_get env2 s ~global_clear:false Env.Middle
@@ -210,7 +210,7 @@ and context_insensitive_term_to_exp kf env t =
   | TUnOp(Neg | BNot as op, t') ->
     let ty = Typing.typ_of_term_operation t in
     let e, env = term_to_exp kf env (Some ty) t' in
-    if Mpz.is_t ty then
+    if Gmpz.is_t ty then
       let name, vname = match op with
 	| Neg -> "__gmpz_neg", "neg"
 	| BNot -> "__gmpz_com", "bnot"
@@ -229,7 +229,7 @@ and context_insensitive_term_to_exp kf env t =
       Cil.new_exp ~loc (UnOp(op, e, ty)), env, false, ""
   | TUnOp(LNot, t) ->
     let ty = Typing.typ_of_term_operation t in
-    if Mpz.is_t ty then
+    if Gmpz.is_t ty then
       (* [!t] is converted into [t == 0] *)
       let zero = Logic_const.tinteger 0 in
       let e, env = 
@@ -246,7 +246,7 @@ and context_insensitive_term_to_exp kf env t =
     let ctx = Some ty in
     let e1, env = term_to_exp kf env ctx t1 in
     let e2, env = term_to_exp kf env ctx t2 in
-    if Mpz.is_t ty then
+    if Gmpz.is_t ty then
       let name = name_of_mpz_arith_bop bop in
       let mk_stmts _ e = [ Misc.mk_call ~loc name [ e; e1; e2 ] ] in
       let name = name_of_binop bop in
@@ -267,7 +267,7 @@ and context_insensitive_term_to_exp kf env t =
     let ctx = Some ty in
     let e1, env = term_to_exp kf env ctx t1 in
     let e2, env = term_to_exp kf env ctx t2 in
-    if Mpz.is_t ty then 
+    if Gmpz.is_t ty then 
       (* TODO: preventing division by zero should not be required anymore.
 	 RTE should do this automatically. *)
       let t = Some t in
@@ -283,7 +283,7 @@ and context_insensitive_term_to_exp kf env t =
 	comparison_to_exp ~loc kf env ~e1:(e2, ty) ~name Eq t2 zero t 
       in
       let mk_stmts _v e = 
-	assert (Mpz.is_t ty);
+	assert (Gmpz.is_t ty);
 	let vis = Env.get_visitor env in
 	let kf = Extlib.the vis#current_kf in
 	let cond = 
@@ -346,8 +346,8 @@ and context_insensitive_term_to_exp kf env t =
 	 second is an integer type, or the reverse *)
       let ty1 = Typing.typ_of_term t1 in
       let ty2 = Typing.typ_of_term t2 in
-      if Mpz.is_t ty1 then Some Cil.longType, Some ty2, ty2
-      else if Mpz.is_t ty2 then Some ty1, Some Cil.longType, ty1
+      if Gmpz.is_t ty1 then Some Cil.longType, Some ty2, ty2
+      else if Gmpz.is_t ty2 then Some ty1, Some Cil.longType, ty1
       else Some ty1, Some ty2, if Cil.isIntegralType ty1 then ty2 else ty1
     in
     let e1, env = term_to_exp kf env ctx1 t1 in
@@ -441,7 +441,7 @@ and comparison_to_exp
       e1, env, ctx
   in
   let e2, env = term_to_exp kf env (Some ctx) t2 in
-  if Mpz.is_t ctx then
+  if Gmpz.is_t ctx then
     let _, e, env =
       Env.new_var
 	~loc
@@ -533,7 +533,7 @@ and at_to_exp env t_opt label e =
     method !vstmt_aux stmt = 
       (* either a standard C affectation or an mpz one according to type of
 	 [e] *) 
-      let new_stmt = Mpz.init_set ~loc (Cil.var res_v) res e in
+      let new_stmt = Gmpz.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
 	 corresponding environment *)

src/plugins/e-acsl/typing.ml

@@ -69,13 +69,13 @@ let typ_of_eacsl_typ = function
        let ty_u = TInt(ikind_of_integer u is_pos, []) in
        Cil.arithmeticConversion ty_l ty_u
      with Cil.Not_representable -> 
-       Mpz.t ())
-  | Z -> Mpz.t ()
+       Gmpz.t ())
+  | Z -> Gmpz.t ()
   | No_integral (Ctype ty) -> ty
   | No_integral ty when Logic_const.is_boolean_type ty -> assert false
   | No_integral (Ltype _) -> Error.not_yet "typing of user-defined logic type"
   | No_integral (Lvar _) -> Error.not_yet "type variable"
-  | No_integral Linteger -> Mpz.t ()
+  | No_integral Linteger -> Gmpz.t ()
   | No_integral Lreal -> TFloat(FLongDouble, [])
   | No_integral (Larrow _) -> Error.not_yet "functional type"
 
@@ -88,7 +88,7 @@ let eacsl_typ_of_typ ty =
       else Z.zero, Cil.max_unsigned_number n
     in
     Interv(l, u)
-  | ty when Mpz.is_t ty -> Z
+  | ty when Gmpz.is_t ty -> Z
   | ty -> No_integral (Ctype ty)
 
 exception Cannot_compare
@@ -164,10 +164,10 @@ let generic_typ (which: < f: 'a. 'a * 'a -> 'a >) t =
   Cil.CurrentLoc.set t.term_loc;
     if Options.Gmp_only.get () then 
       let ty = match t.term_type with
-	| Linteger -> Mpz.t ()
-	| Ctype ty when Cil.isIntegralType ty -> Mpz.t ()
+	| Linteger -> Gmpz.t ()
+	| Ctype ty when Cil.isIntegralType ty -> Gmpz.t ()
 	| Ctype ty -> ty
-	| Ltype _ as ty when Logic_const.is_boolean_type ty -> Mpz.t ()
+	| Ltype _ as ty when Logic_const.is_boolean_type ty -> Gmpz.t ()
 	| Ltype _ -> Error.not_yet "typing of user-defined logic type"
 	| Lvar _ -> Error.not_yet "type variable"
 	| Lreal -> TFloat(FLongDouble, [])
@@ -327,7 +327,7 @@ let rec type_term t =
       let n = Z.div (Bit_utils.max_bit_address ()) (Z.of_int 8) in
       let ty =
         try TInt(ikind_of_integer n true, [])
-        with Cil.Not_representable -> Mpz.t ()
+        with Cil.Not_representable -> Gmpz.t ()
       in
       dup eacsl_typ_of_typ ty
     | Tblock_length(_, t) ->
@@ -335,7 +335,7 @@ let rec type_term t =
       let n = Z.div (Bit_utils.max_bit_size ()) (Z.of_int 8) in
       let ty =
         try TInt(ikind_of_integer n true, [])
-        with Cil.Not_representable -> Mpz.t ()
+        with Cil.Not_representable -> Gmpz.t ()
       in
       dup eacsl_typ_of_typ ty
     | Tnull -> dup int_to_interv 0
@@ -533,15 +533,15 @@ let context_sensitive ~loc ?name env ctx is_mpz_string t_opt e =
 	?name
 	env
 	t_opt
-	(Mpz.t ())
-	(fun lv v -> [ Mpz.init_set ~loc (Cil.var lv) v e ])
+	(Gmpz.t ())
+	(fun lv v -> [ Gmpz.init_set ~loc (Cil.var lv) v e ])
     in
     e, env
   in
   let do_int_ctx ty =
     (* handle a C-integer context *)
     let e, env = if is_mpz_string then mk_mpz e else e, env in
-    if (Mpz.is_t ty || is_mpz_string) then
+    if (Gmpz.is_t ty || is_mpz_string) then
       (* we get an mpz, but it fits into a C integer: convert it *)
       let fname, new_ty = 
 	if Cil.isSignedInteger ty then 
@@ -566,14 +566,14 @@ let context_sensitive ~loc ?name env ctx is_mpz_string t_opt e =
 	  e),
       env
   in
-  if Mpz.is_t ctx then
-    if Mpz.is_t ty then
+  if Gmpz.is_t ctx then
+    if Gmpz.is_t ty then
       e, env
     else
       (* Convert the C integer into a mpz. 
 	 Remember: very long integer constants have been temporary converted
 	 into strings;
-	 also possible to get a non integralType (or Mpz.t) with a non-one in
+	 also possible to get a non integralType (or Gmpz.t) with a non-one in
 	 the case of \null *)
       let e = 
 	if Cil.isIntegralType ty || is_mpz_string then e
@@ -586,13 +586,13 @@ let context_sensitive ~loc ?name env ctx is_mpz_string t_opt e =
 let principal_type t1 t2 = 
   let ty1 = typ_of_term t1 in
   let ty2 = typ_of_term t2 in
-  (* possible to get an integralType (or Mpz.t) from a non-one in the case of
+  (* possible to get an integralType (or Gmpz.t) from a non-one in the case of
      \null *)
   if Cil.isIntegralType ty1 then
     if Cil.isIntegralType ty2 then Cil.arithmeticConversion ty1 ty2
-    else if Mpz.is_t ty2 then ty2 else ty1
-  else if Mpz.is_t ty1 then
-    if Cil.isIntegralType ty2 || Mpz.is_t ty2 then ty1 else ty2
+    else if Gmpz.is_t ty2 then ty2 else ty1
+  else if Gmpz.is_t ty1 then
+    if Cil.isIntegralType ty2 || Gmpz.is_t ty2 then ty1 else ty2
   else 
     ty2