diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli index 2109d348982bcead8a6af992c72e6e5eb76d9851..7ee24149cc1af12a70991cd3d27868c4b18d88d6 100644 --- a/src/plugins/value/Eva.mli +++ b/src/plugins/value/Eva.mli @@ -68,6 +68,10 @@ module Results: sig val equality_class : Cil_types.exp -> request -> Cil_types.exp list result val as_cvalue_model : request -> Cvalue.Model.t result + (* Dependencies *) + val expr_deps : Cil_types.exp -> request -> Locations.Zone.t + val lval_deps : Cil_types.lval -> request -> Locations.Zone.t + (* Evaluation *) val eval_var : Cil_types.varinfo -> request -> value evaluation val eval_lval : Cil_types.lval -> request -> value evaluation diff --git a/src/plugins/value/register.mli b/src/plugins/value/register.mli index c27dd17263fd3f5deb3581b5ebdd0f6c3b2674f5..c0758d9b6fc6f1cfc03e77f042f5cee0ca93a1f2 100644 --- a/src/plugins/value/register.mli +++ b/src/plugins/value/register.mli @@ -20,6 +20,10 @@ (* *) (**************************************************************************) -(** Functions of the Value plugin registered in {!Db}. +(** Functions of the Value plugin registered in {!Db}. Only two functions + are exported. *) - Nothing is exported. *) +val eval_deps : Cvalue.Model.t * Locals_scoping.clobbered_set -> + Cil_types.exp -> Locations.Zone.t +val eval_deps_lval : Cvalue.Model.t * Locals_scoping.clobbered_set -> + Cil_types.lval -> Locations.Zone.t diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml index 9cb35d245f0a712d43f3ef2b53e281c8fa642686..cd0ecab0cfde54f663bf0c44aa62a73e4cb21703 100644 --- a/src/plugins/value/utils/results.ml +++ b/src/plugins/value/utils/results.ml @@ -357,7 +357,7 @@ struct (* Evaluation *) - let eval_lval lval req= + let eval_lval lval req = let eval state = A.Eval.copy_lvalue state lval in LValue (Response.map eval (get req)) @@ -486,6 +486,22 @@ struct match r with | `Bottom -> true | `Top | `Value () -> false + + (* Dependencies *) + + let lval_deps lval req = + let compute_deps cvalue = + Register.eval_deps_lval (cvalue, Locals_scoping.bottom ()) lval + in + req |> as_cvalue_model |> + Result.fold ~error:(fun _ -> Locations.Zone.bottom) ~ok:compute_deps + + let expr_deps exp req = + let compute_deps cvalue = + Register.eval_deps (cvalue, Locals_scoping.bottom ()) exp + in + req |> as_cvalue_model |> + Result.fold ~error:(fun _ -> Locations.Zone.bottom) ~ok:compute_deps end @@ -519,6 +535,17 @@ let as_cvalue_model req = E.as_cvalue_model req +(* Depedencies *) + +let expr_deps exp req = + let module E = Make () in + E.expr_deps exp req + +let lval_deps lval req = + let module E = Make () in + E.lval_deps lval req + + (* Evaluation *) module type Lvaluation = diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli index 3d13c3c74d0172125fef7e3bd2a15a5831536a50..3720534eb91d270824b9ee8ec9288ae2288d6978 100644 --- a/src/plugins/value/utils/results.mli +++ b/src/plugins/value/utils/results.mli @@ -71,6 +71,10 @@ val fold_callstacks : (callstack -> request -> 'a -> 'a) -> 'a -> request -> 'a val equality_class : Cil_types.exp -> request -> Cil_types.exp list result val as_cvalue_model : request -> Cvalue.Model.t result +(* Dependencies *) +val expr_deps : Cil_types.exp -> request -> Locations.Zone.t +val lval_deps : Cil_types.lval -> request -> Locations.Zone.t + (* Evaluation *) val eval_var : Cil_types.varinfo -> request -> value evaluation val eval_lval : Cil_types.lval -> request -> value evaluation