From e606c07cc556695bf786e2d6fa865e02d4fa8619 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 2 Dec 2020 14:26:12 +0100
Subject: [PATCH] [eva] export evaluation and condition reductions
---
src/plugins/value/engine/analysis.ml | 8 +++++++-
src/plugins/value/engine/analysis.mli | 3 ++-
2 files changed, 9 insertions(+), 2 deletions(-)
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index 06c72bf5099..256e3db49ab 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -40,10 +40,11 @@ module type Results = sig
val eval_lval_to_loc: state -> lval -> location evaluated
val eval_function_exp:
state -> ?args:exp list -> exp -> kernel_function list evaluated
+ val assume_cond : stmt -> state -> exp -> bool -> state or_bottom
end
module type S = sig
- include Abstractions.S
+ include Abstractions.Eva
include Results with type state := Dom.state
and type value := Val.t
and type location := Loc.location
@@ -95,6 +96,11 @@ module Make (Abstract: Abstractions.S) = struct
let eval_function_exp state ?args e =
Eval.eval_function_exp e ?args state >>=: (List.map fst)
+ let assume_cond stmt state cond positive =
+ fst (Eval.reduce state cond positive) >>- fun valuation ->
+ let dval = Eval.to_domain_valuation valuation in
+ Dom.assume stmt cond positive dval state
+
end
diff --git a/src/plugins/value/engine/analysis.mli b/src/plugins/value/engine/analysis.mli
index e96f3ed5ea1..6f85061797c 100644
--- a/src/plugins/value/engine/analysis.mli
+++ b/src/plugins/value/engine/analysis.mli
@@ -40,6 +40,7 @@ module type Results = sig
val eval_lval_to_loc: state -> lval -> location evaluated
val eval_function_exp:
state -> ?args:exp list -> exp -> kernel_function list evaluated
+ val assume_cond : stmt -> state -> exp -> bool -> state or_bottom
end
@@ -55,7 +56,7 @@ end
module type S = sig
- include Abstractions.S
+ include Abstractions.Eva
include Results with type state := Dom.state
and type value := Val.t
and type location := Loc.location
--
GitLab