[e-acsl] first review

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

@@ -83,13 +83,10 @@ let rec get_assigns_from ~loc env lprofile lv =
    For the argument [__e_acsl_mpz_t *__retres_arg], this function generates the
    expression [( *__retres_arg )[0]]. For a struct argument, this function just
    generates the variable corresponding to the argument. *)
-let get_assigned_var ~loc vi ret_gmp =
+let get_assigned_var ~loc ~is_gmp vi =
   let var =
-    if ret_gmp then
-      Smart_exp.lval
-        ~loc
-        (Mem
-           (Smart_exp.lval  ~loc (Var vi, NoOffset)),
-         (Index (Cil.zero ~loc, NoOffset)))
-    else Smart_exp.lval ~loc (Var vi, NoOffset)
-  in Logic_utils.expr_to_term 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

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

@@ -32,6 +32,6 @@ val get_assigns_from :
    the result of a logic function *)
 
 val get_assigned_var :
-  loc:Cil_types.location -> Cil_types.varinfo -> bool -> Cil_types.term
+  loc:Cil_types.location -> is_gmp:bool -> Cil_types.varinfo -> Cil_types.term
 (* @returns the expression that gets assigned when the result of the function is
    passed as an additional argument *)

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

@@ -56,15 +56,13 @@ let term_to_exp_ref
 (* @return true iff the result of the function is provided by reference as the
    first extra argument at each call *)
 let result_as_extra_argument typ =
-  let is_composite = function
+  let is_composite typ =
+    match Cil.unrollType typ with
     | TComp _ | TPtr _ | TArray _ -> true
     | TInt _ | TVoid _  | TFloat _ | TFun _ | TNamed _ | TEnum _
     | TBuiltin_va_list _ -> false
   in
-  Gmp_types.Z.is_t typ ||
-  is_composite typ
-(* TODO: to be extended to any compound type? E.g. returning a struct is not
-   good practice... *)
+  Gmp_types.Z.is_t typ || Gmp_types.Q.is_t typ || is_composite typ
 
 (*****************************************************************************)
 (****************** Generation of function bodies ****************************)
@@ -158,7 +156,8 @@ let generate_kf ~loc fname env ret_ty params_ty params_ival li =
   in
   (* build the varinfo storing the result *)
   let res_as_extra_arg = result_as_extra_argument ret_ty in
-  let ret_gmp = Gmp_types.Z.is_t ret_ty in
+  let is_mpz = Gmp_types.Z.is_t ret_ty in
+  let is_mpq = Gmp_types.Q.is_t ret_ty in
   let ret_vi, ret_ty, params_with_ret, params_ty_with_ret =
     let vname = "__retres" in
     if res_as_extra_arg then
@@ -217,7 +216,7 @@ let generate_kf ~loc fname env ret_ty params_ty params_ival li =
     let assigned_var =
       Logic_const.new_identified_term
         (if res_as_extra_arg then
-           Assigns.get_assigned_var ~loc ret_vi ret_gmp
+           Assigns.get_assigned_var ~loc ~is_gmp:(is_mpz || is_mpq) ret_vi
          else
            Logic_const.tresult fundec.svar.vtype)
     in

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

@@ -71,6 +71,12 @@ let lnot ~loc e =
 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)))
+
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."

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

@@ -46,6 +46,8 @@ val lnot: loc:location -> exp -> exp
 val null: loc:location -> exp
 (** [null ~loc] creates an expression to represent the NULL pointer. *)
 
+val mem: loc:location -> varinfo -> exp
+
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."