From 5bd9c8c9eca282626dd90775f228b284c56fd54e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 18 Feb 2019 11:24:31 +0100
Subject: [PATCH] [Eva] Fixes simple_memory: do not fail on top locations.
Catches Abstract_interp.Error_Top when folding a location.
When updating the state from a valuation, do not reduce the value for a location
that is not a singleton: the state can instead be left unchanged, while the
binding of an imprecise location cannot reduce the state.
---
src/plugins/value/domains/simple_memory.ml | 16 +++++++++++-----
1 file changed, 11 insertions(+), 5 deletions(-)
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index 9612b41755a..4f27194587e 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -141,7 +141,8 @@ module Make_Memory (Value: Value) = struct
else add b v state
| Imprecise -> remove b state
in
- Location_Bits.fold_topset_ok aux_base loc state
+ try Location_Bits.fold_topset_ok aux_base loc state
+ with Abstract_interp.Error_Top -> empty
let remove_variables vars state =
let remove_variable state v = remove (Base.of_varinfo v) state in
@@ -161,9 +162,11 @@ module Make_Memory (Value: Value) = struct
| Precise -> Bottom.join Value.join r (`Value (find_or_top b state))
| Imprecise -> `Value Value.top
in
- match Location_Bits.fold_topset_ok aux_base loc `Bottom with
- | `Bottom -> Value.top (* does not happen if the location is not empty *)
- | `Value v -> v
+ try
+ match Location_Bits.fold_topset_ok aux_base loc `Bottom with
+ | `Bottom -> Value.top (* does not happen if the location is not empty *)
+ | `Value v -> v
+ with Abstract_interp.Error_Top -> Value.top
end
@@ -234,7 +237,10 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
| Lval lv -> begin
match Valuation.find_loc valuation lv with
| `Top -> state
- | `Value {loc; typ} -> bind_loc loc typ record.value.v state
+ | `Value {loc; typ} ->
+ if Precise_locs.cardinal_zero_or_one loc
+ then bind_loc loc typ record.value.v state
+ else state
end
| _ -> state
--
GitLab