From 71c4ead70a492767e29f627bea29af72287e8d6f Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Wed, 10 Aug 2022 18:01:36 +0200
Subject: [PATCH] [e-acsl] first review
---
src/plugins/e-acsl/src/code_generator/assigns.ml | 15 ++++++---------
src/plugins/e-acsl/src/code_generator/assigns.mli | 2 +-
.../e-acsl/src/code_generator/logic_functions.ml | 13 ++++++-------
.../e-acsl/src/code_generator/smart_exp.ml | 6 ++++++
.../e-acsl/src/code_generator/smart_exp.mli | 2 ++
5 files changed, 21 insertions(+), 17 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/assigns.ml b/src/plugins/e-acsl/src/code_generator/assigns.ml
index bf8e2dddc4c..71a54f001ca 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 650214584a2..cf064eccd35 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 a0b88104c04..a513853145e 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 bd7c20cc87f..9ac13a267b9 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 a2f1dbd8200..d57e74be629 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 ../../../../.."
--
GitLab