[E-ACSL] rename Gmp.affect to Gmp.assign

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

@@ -89,7 +89,7 @@ let generic_affect ~loc fname lv ev e =
   end else
     Smart_stmt.assigns ~loc:e.eloc ~result:lv e
 
-let affect ~loc lv ev e =
+let assign ~loc lv ev e =
   let fname =
     let ty = Cil.typeOf ev in
     if Gmp_types.Z.is_t ty then "__gmpz_set"
@@ -133,7 +133,7 @@ let init_set ~loc lv ev e =
     Smart_stmt.block_stmt
       (Cil.mkBlock
          [ init ~loc ev ;
-           affect ~loc lv ev e ])
+           assign ~loc lv ev e ])
   else
     mpz_init_set ""
 
@@ -338,7 +338,7 @@ module Q = struct
           (Gmp_types.Q.t ())
           (fun vi vi_e ->
              [ init ~loc vi_e ;
-               affect ~loc (Cil.var vi) vi_e e ])
+               assign ~loc (Cil.var vi) vi_e e ])
       in
       e, env
 

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

@@ -35,8 +35,8 @@ val init_set: loc:location -> lval -> exp -> exp -> stmt
 val clear: location -> exp -> stmt
 (** build stmt [mpz_clear(v)] or [mpq_clear(v)] depending on typ of [v] *)
 
-val affect: loc:location -> lval -> exp -> exp -> stmt
-(** [affect x_as_lv x_as_exp e] builds stmt [x = e] or [mpz_set*(e)]
+val assign: loc:location -> lval -> exp -> exp -> stmt
+(** [assign x_as_lv x_as_exp e] builds stmt [x = e] or [mpz_set*(e)]
     or [mpq_set*(e)] with the good function 'set'
     according to the type of [e] *)
 

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

@@ -321,7 +321,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
     let e1, _, env = term_to_exp kf (Env.push env) t1 in
     let init_blk, env = Env.pop_and_get
         env
-        (Gmp.affect ~loc:e1.eloc lv_x x e1)
+        (Gmp.assign ~loc:e1.eloc lv_x x e1)
         ~global_clear:false
         Env.Middle
     in
@@ -362,7 +362,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
     let incr, _, env = term_to_exp kf (Env.push env) tlv_one in
     let next_blk, env = Env.pop_and_get
         env
-        (Gmp.affect ~loc:incr.eloc lv_x x incr)
+        (Gmp.assign ~loc:incr.eloc lv_x x incr)
         ~global_clear:false
         Env.Middle
     in
@@ -429,6 +429,6 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
 
 (*
 Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
 End:
 *)

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

@@ -201,7 +201,7 @@ and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
     let e_lbd, _, env = to_exp ~adata:Assert.no_data kf env lt in
     let lbd_stmt,env =
       Env.pop_and_get env
-        (Gmp.affect ~loc (Cil.var lbd_as_varinfo) lbd_as_exp e_lbd)
+        (Gmp.assign ~loc (Cil.var lbd_as_varinfo) lbd_as_exp e_lbd)
         ~global_clear:false Env.Middle
     in
     (* statement construction *)