[e-acsl] second review

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

@@ -84,9 +84,5 @@ let rec get_assigns_from ~loc env lprofile lv =
    expression [( *__retres_arg )[0]]. For a struct argument, this function just
    generates the variable corresponding to the argument. *)
 let get_assigned_var ~loc ~is_gmp vi =
-  let var =
-    if is_gmp
-    then Smart_exp.mem ~loc vi
-    else Smart_exp.lval ~loc (Cil.var vi)
-  in
-  Logic_utils.expr_to_term var
+  let var = if is_gmp then Smart_exp.mem ~loc vi else Cil.evar ~loc vi
+  in Logic_utils.expr_to_term var

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

@@ -72,10 +72,9 @@ let null ~loc =
   Cil.mkCast ~newt:(TPtr (TVoid [], [])) (Cil.zero ~loc)
 
 let mem ~loc vi =
-  lval ~loc
-    (Cil.mkMem
-       ~addr:(lval ~loc (Var vi, NoOffset))
-       ~off:(Index (Cil.zero ~loc, NoOffset)))
+  lval
+    ~loc
+    (Cil.mkMem ~addr:(Cil.evar ~loc vi) ~off:(Index (Cil.zero ~loc, NoOffset)))
 
 (*
 Local Variables:

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

@@ -47,7 +47,8 @@ val null: loc:location -> exp
 (** [null ~loc] creates an expression to represent the NULL pointer. *)
 
 val mem: loc:location -> varinfo -> exp
-
+(** [mem ~loc v] creates an expression to represent the array access to the
+    first location of v *)
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."

src/plugins/e-acsl/tests/arith/functions.c

@@ -80,7 +80,7 @@ int main(void) {
 
   /*@ assert f_sum (100) == 100; */;
 
-  /*@ assert over(1., 2.) == 1./2.; */;
+  /*@ assert over(1., 2.) == 0.5; */;
 
   // not yet supported
   /* /\*@ assert p_notyet(27); *\/ ; */

src/plugins/e-acsl/tests/arith/oracle/gen_functions.c

@@ -411,28 +411,20 @@ int main(void)
   {
     __e_acsl_mpq_t __gen_e_acsl_over_2;
     __e_acsl_mpq_t __gen_e_acsl__11;
-    __e_acsl_mpq_t __gen_e_acsl__12;
-    __e_acsl_mpq_t __gen_e_acsl_div_3;
     int __gen_e_acsl_eq_2;
     __e_acsl_assert_data_t __gen_e_acsl_assert_data_15 =
       {.values = (void *)0};
     __gen_e_acsl_over(& __gen_e_acsl_over_2,1.,2.);
     __gmpq_init(__gen_e_acsl__11);
-    __gmpq_set_d(__gen_e_acsl__11,1.);
-    __gmpq_init(__gen_e_acsl__12);
-    __gmpq_set_d(__gen_e_acsl__12,2.);
-    __gmpq_init(__gen_e_acsl_div_3);
-    __gmpq_div(__gen_e_acsl_div_3,
-               (__e_acsl_mpq_struct const *)(__gen_e_acsl__11),
-               (__e_acsl_mpq_struct const *)(__gen_e_acsl__12));
+    __gmpq_set_d(__gen_e_acsl__11,0.5);
     __gen_e_acsl_eq_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_over_2),
-                                   (__e_acsl_mpq_struct const *)(__gen_e_acsl_div_3));
+                                   (__e_acsl_mpq_struct const *)(__gen_e_acsl__11));
     __e_acsl_assert_register_mpq(& __gen_e_acsl_assert_data_15,
                                  "over(1., 2.)",
                                  (__e_acsl_mpq_struct const *)(__gen_e_acsl_over_2));
     __gen_e_acsl_assert_data_15.blocking = 1;
     __gen_e_acsl_assert_data_15.kind = "Assertion";
-    __gen_e_acsl_assert_data_15.pred_txt = "over(1., 2.) == 1. / 2.";
+    __gen_e_acsl_assert_data_15.pred_txt = "over(1., 2.) == 0.5";
     __gen_e_acsl_assert_data_15.file = "functions.c";
     __gen_e_acsl_assert_data_15.fct = "main";
     __gen_e_acsl_assert_data_15.line = 83;
@@ -440,10 +432,8 @@ int main(void)
     __e_acsl_assert_clean(& __gen_e_acsl_assert_data_15);
     __gmpq_clear(__gen_e_acsl_over_2);
     __gmpq_clear(__gen_e_acsl__11);
-    __gmpq_clear(__gen_e_acsl__12);
-    __gmpq_clear(__gen_e_acsl_div_3);
   }
-  /*@ assert over(1., 2.) == 1. / 2.; */ ;
+  /*@ assert over(1., 2.) == 0.5; */ ;
   __retres = 0;
   __e_acsl_memory_clean();
   return __retres;