From 3ed8a0781d88db70a3653fa6712ae3a2ed5e9ad5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 31 Jan 2020 11:21:48 +0100
Subject: [PATCH] [Eva] Eval_term: renames [econstant] into [inject_no_deps]
and fixes a comment.
---
src/plugins/value/legacy/eval_terms.ml | 15 ++++++++-------
1 file changed, 8 insertions(+), 7 deletions(-)
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index c9607a9d98d..9a9fb45daa4 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -472,20 +472,21 @@ let is_noop_cast ~src_typ ~dst_typ =
| Some (TSPtr _), Some (TSPtr _) -> true
| _ -> false
-let econstant typ cvalue =
+(* Injects [cvalue] as an eval_result of type [typ] with no dependencies. *)
+let inject_no_deps typ cvalue =
{ etype = typ;
eunder = under_from_over cvalue;
eover = cvalue;
ldeps = empty_logic_deps }
-(* Note: non-constant integers can happen e.g. for sizeof of structures of an unknown size. *)
-let einteger = econstant Cil.intType
+(* Integer result with no memory dependencies: constants, sizeof & alignof,
+ and values of logic variables.*)
+let einteger = inject_no_deps Cil.intType
(* Note: some reals cannot be exactly represented as floats; in which
case we do not know their under-approximation. *)
-let efloating_point etype fval = econstant etype (Cvalue.V.inject_float fval)
-let ereal = efloating_point Cil.doubleType
-let efloat = efloating_point Cil.floatType
+let ereal fval = inject_no_deps Cil.doubleType (Cvalue.V.inject_float fval)
+let efloat fval = inject_no_deps Cil.floatType (Cvalue.V.inject_float fval)
let is_true = function
| `True | `TrueReduced _ -> true
@@ -798,7 +799,7 @@ let rec eval_term ~alarm_mode env t =
let cvalue = LogicVarEnv.find logic_var env.logic_vars in
if logic_var.lv_type = Linteger
then einteger cvalue
- else econstant Cil.doubleType cvalue
+ else inject_no_deps Cil.doubleType cvalue
| TLval tlval ->
let lval = eval_tlval ~alarm_mode env tlval in
--
GitLab