Skip to content
Snippets Groups Projects
Commit f53e7dc4 authored by Maxime Jacquemin's avatar Maxime Jacquemin Committed by David Bühler
Browse files

[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.
parent 465d31ba
No related branches found
No related tags found
No related merge requests found
...@@ -337,8 +337,9 @@ let as_cvalue_model req = ...@@ -337,8 +337,9 @@ let as_cvalue_model req =
module type Evaluation = module type Evaluation =
sig sig
type 'callstack evaluation type 'a evaluation
val v : unrestricted_response evaluation type restriction
val v : restriction evaluation
val as_cvalue : 'callstack evaluation -> Main_values.CVal.t result val as_cvalue : 'callstack evaluation -> Main_values.CVal.t result
val as_functions : 'callstack evaluation -> val as_functions : 'callstack evaluation ->
Cil_types.kernel_function list result Cil_types.kernel_function list result
...@@ -347,21 +348,32 @@ end ...@@ -347,21 +348,32 @@ end
type evaluation = (module Evaluation) type evaluation = (module Evaluation)
type lvaluation type lvaluation
let eval_lval lval req = let eval_lval, eval_exp =
(module struct let module M = Make () in
include Make () let open Response in
let v = eval_lval lval req let build = function
end : Evaluation) | `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 = let eval_var vi req =
eval_lval (Cil.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 = let eval_address _lval _req =
raise Not_implemented raise Not_implemented
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment