From 5a746267492c58861a033648a580ae1aa9899ccc Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Thu, 11 Aug 2022 09:42:48 +0200
Subject: [PATCH] [e-acsl] second review
---
.../e-acsl/src/code_generator/assigns.ml | 8 ++------
.../e-acsl/src/code_generator/smart_exp.ml | 7 +++----
.../e-acsl/src/code_generator/smart_exp.mli | 3 ++-
src/plugins/e-acsl/tests/arith/functions.c | 2 +-
.../e-acsl/tests/arith/oracle/gen_functions.c | 18 ++++--------------
5 files changed, 12 insertions(+), 26 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/assigns.ml b/src/plugins/e-acsl/src/code_generator/assigns.ml
index 71a54f001ca..1febf4acf41 100644
--- a/src/plugins/e-acsl/src/code_generator/assigns.ml
+++ b/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
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 9ac13a267b9..3475ed66929 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_exp.ml
+++ b/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:
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 d57e74be629..b2a5e5b03f2 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_exp.mli
+++ b/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 ../../../../.."
diff --git a/src/plugins/e-acsl/tests/arith/functions.c b/src/plugins/e-acsl/tests/arith/functions.c
index 9c327c0e1b9..ead203551b4 100644
--- a/src/plugins/e-acsl/tests/arith/functions.c
+++ b/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); *\/ ; */
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
index 8699808b755..ca9e702ccf9 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
+++ b/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;
--
GitLab