From f53e7dc4dddfcb18979ce18454be03f060db0e62 Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime2.jacquemin@gmail.com>
Date: Fri, 26 Mar 2021 11:01:57 +0100
Subject: [PATCH] [Eva] api: Something bothered me
The evaluation could only contain unrestricted_response evaluation,
which was quite bothering as it makes the GADT useless.
I've modified it to be able to represent restricted_to_callstack
evaluation as well.
The modification is propagated to eval_lval and eval_exp.
---
src/plugins/value/utils/results.ml | 38 ++++++++++++++++++++----------
1 file changed, 25 insertions(+), 13 deletions(-)
diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml
index acd45de0ea3..a9ea9e29922 100644
--- a/src/plugins/value/utils/results.ml
+++ b/src/plugins/value/utils/results.ml
@@ -337,8 +337,9 @@ let as_cvalue_model req =
module type Evaluation =
sig
- type 'callstack evaluation
- val v : unrestricted_response evaluation
+ type 'a evaluation
+ type restriction
+ val v : restriction evaluation
val as_cvalue : 'callstack evaluation -> Main_values.CVal.t result
val as_functions : 'callstack evaluation ->
Cil_types.kernel_function list result
@@ -347,21 +348,32 @@ end
type evaluation = (module Evaluation)
type lvaluation
-let eval_lval lval req =
- (module struct
- include Make ()
- let v = eval_lval lval req
- end : Evaluation)
+let eval_lval, eval_exp =
+ let module M = Make () in
+ let open Response in
+ let build = function
+ | `LValue (_, Consolidated _)
+ | `Value (Consolidated _) as eval ->
+ (module struct
+ include M
+ type restriction = unrestricted_response
+ let v = eval
+ end : Evaluation)
+ | `LValue (_, (ByCallstack _ | Top | Bottom))
+ | `Value (ByCallstack _ | Top | Bottom) as eval ->
+ (module struct
+ include M
+ type restriction = restricted_to_callstack
+ let v = eval
+ end : Evaluation)
+ in
+ let eval_lval lval req = build @@ M.eval_lval lval req in
+ let eval_exp exp req = build @@ M.eval_exp exp req in
+ eval_lval, eval_exp
let eval_var vi req =
eval_lval (Cil.var vi) req
-let eval_exp exp req =
- (module struct
- include Make ()
- let v = eval_exp exp req
- end : Evaluation)
-
let eval_address _lval _req =
raise Not_implemented
--
GitLab