From f5ee5c32b3389db16d0df4eb6ee51c3837adf36f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 23 Jan 2020 10:55:26 +0100
Subject: [PATCH] [Eva] Evaluation: renames low_context into fast_eval_context.
---
src/plugins/value/engine/evaluation.ml | 16 ++++++++--------
1 file changed, 8 insertions(+), 8 deletions(-)
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index 7ab9e0258c4..c9ecc4766a4 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -1120,7 +1120,7 @@ module Make
(* Context for a fast forward evaluation with minimal precision:
no subdivisions and no calls to the oracle. *)
- let low_context state =
+ let fast_eval_context state =
let remaining_fuel = no_fuel in
let subdivision = 0 in
{ state; subdivision; remaining_fuel; oracle }
@@ -1160,7 +1160,7 @@ module Make
let evaluate_for_reduction state expr =
try `Value (Cache.find' !cache expr)
with Not_found ->
- fst (forward_eval (low_context state) expr) >>-: fun _ ->
+ fst (forward_eval (fast_eval_context state) expr) >>-: fun _ ->
try Cache.find' !cache expr
with Not_found -> assert false
@@ -1352,7 +1352,7 @@ module Make
| _ ->
let reduce_valid_index = true in
let typ_lval = Cil.typeOf_pointed (Cil.typeOf expr) in
- let context = low_context state in
+ let context = fast_eval_context state in
fst (eval_offset context ~reduce_valid_index typ_lval offset)
>>- fun (loc_offset, _, _) ->
find_val expr >>- fun value ->
@@ -1369,7 +1369,7 @@ module Make
| Index (exp, remaining) ->
find_val exp >>- fun v ->
let typ_pointed = Cil.typeOf_array_elem typ in
- let context = low_context state in
+ let context = fast_eval_context state in
fst (eval_offset context ~reduce_valid_index:true typ_pointed remaining)
>>- fun (rem, _, _) ->
Loc.backward_index typ_pointed v rem loc_offset >>- fun (v', rem') ->
@@ -1410,7 +1410,7 @@ module Make
match expr.enode with
| Lval lval -> second_eval_lval state lval value
| _ ->
- fst (internal_forward_eval (low_context state) expr)
+ fst (internal_forward_eval (fast_eval_context state) expr)
>>-: fun (v, _, _) -> v
in
new_value >>- fun evaled ->
@@ -1435,7 +1435,7 @@ module Make
then
let for_writing = false
and reduction = true
- and context = low_context state in
+ and context = fast_eval_context state in
fst (reduced_lval_to_loc context ~for_writing ~reduction lval)
>>-: fun (loc, _, _, _) ->
(* TODO: Loc.narrow *)
@@ -1448,7 +1448,7 @@ module Make
else `Value ()
in
evaloc >>- fun () ->
- fst (eval_lval (low_context state) lval) >>- fun (record, _, _) ->
+ fst (eval_lval (fast_eval_context state) lval) >>- fun (record, _, _) ->
record.value.v
and recursive_descent state expr =
@@ -1565,7 +1565,7 @@ module Make
(* Avoids reduce_by_cond_enumerate on volatile expressions. *)
if volatile then `Value !cache
else
- let context = low_context state in
+ let context = fast_eval_context state in
Subdivided_Evaluation.reduce_by_enumeration context !cache expr false
let assume ?valuation:(valuation=Cache.empty) state expr value =
--
GitLab