diff --git a/src/plugins/e-acsl/src/code_generator/assigns.ml b/src/plugins/e-acsl/src/code_generator/assigns.ml index bf8e2dddc4c26c05726d57b3a036a4d89bf241ee..71a54f001ca44869fd1caeab286aab509ba48656 100644 --- a/src/plugins/e-acsl/src/code_generator/assigns.ml +++ b/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 diff --git a/src/plugins/e-acsl/src/code_generator/assigns.mli b/src/plugins/e-acsl/src/code_generator/assigns.mli index 650214584a21773db297e2562976d37c4b00eae4..cf064eccd35dbb3023f8f600750e0e0e600299ce 100644 --- a/src/plugins/e-acsl/src/code_generator/assigns.mli +++ b/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 *) diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml index a0b88104c046859c2a2064e7e96a1acbeff66c82..a513853145eec9a2a931b4ffc70c74f8284d826b 100644 --- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml +++ b/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 diff --git a/src/plugins/e-acsl/src/code_generator/smart_exp.ml b/src/plugins/e-acsl/src/code_generator/smart_exp.ml index bd7c20cc87f4316a8d3a07befb042b97ec5a31ea..9ac13a267b9595df53524f073be70673ba10a938 100644 --- a/src/plugins/e-acsl/src/code_generator/smart_exp.ml +++ b/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 ../../../../.." diff --git a/src/plugins/e-acsl/src/code_generator/smart_exp.mli b/src/plugins/e-acsl/src/code_generator/smart_exp.mli index a2f1dbd82002aea2d8ecbc7a4ea03cf42ec0df3a..d57e74be62926ecc2fea02ff0d30812b583042bc 100644 --- a/src/plugins/e-acsl/src/code_generator/smart_exp.mli +++ b/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 ../../../../.."