diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli index dd7a35736d26776ebcd37743056f9c477bb04d7f..7872eb90937fc538aedbf38dbeff86502fb08a27 100644 --- a/src/plugins/value/Eva.mli +++ b/src/plugins/value/Eva.mli @@ -70,8 +70,9 @@ module Results: sig 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 + val expr_deps : Cil_types.exp -> request -> Locations.Zone.t (* The zone of bits read to evaluate the expression, including adresses computation *) + val lval_deps : Cil_types.lval -> request -> Locations.Zone.t (* The zone of bits read to evaluate the lvalue, including lvalue zone itself *) + val address_deps : Cil_types.lval -> request -> Locations.Zone.t (* The zone of bits read to evaluate the lvalue, excluding the lvalue zone itself *) (* Evaluation *) val eval_var : Cil_types.varinfo -> request -> value evaluation diff --git a/src/plugins/value/register.mli b/src/plugins/value/register.mli index c0758d9b6fc6f1cfc03e77f042f5cee0ca93a1f2..8dd1c29c58ba6d614d2485d39ca054f4c78d6bd7 100644 --- a/src/plugins/value/register.mli +++ b/src/plugins/value/register.mli @@ -23,7 +23,6 @@ (** Functions of the Value plugin registered in {!Db}. Only two functions are 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 +val eval_deps : Cvalue_domain.State.t -> Cil_types.exp -> Locations.Zone.t +val eval_deps_lval : Cvalue_domain.State.t -> Cil_types.lval -> Locations.Zone.t +val eval_deps_addr : Cvalue_domain.State.t -> Cil_types.lval -> Locations.Zone.t diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml index 0e045ae21ecfddca0f8211235998ee67c29dafcb..00bdb7712ada85c0c153f704d5fa3bc5e8428fee 100644 --- a/src/plugins/value/utils/results.ml +++ b/src/plugins/value/utils/results.ml @@ -511,6 +511,14 @@ struct in req |> as_cvalue_model |> Result.fold ~error:(fun _ -> Locations.Zone.bottom) ~ok:compute_deps + + let address_deps lval req = + let compute_deps cvalue = + Register.eval_deps_addr (cvalue, Locals_scoping.bottom ()) lval + in + req |> as_cvalue_model |> + Result.fold ~error:(fun _ -> Locations.Zone.bottom) ~ok:compute_deps + end @@ -554,6 +562,10 @@ let lval_deps lval req = let module E = Make () in E.lval_deps lval req +let address_deps lval req = + let module E = Make () in + E.address_deps lval req + (* Evaluation *) diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli index 6db2025dfb7069d2444edb3a8cfa1fb88247a374..d4030ff471da2bfb95b2324b363c78d391b78f63 100644 --- a/src/plugins/value/utils/results.mli +++ b/src/plugins/value/utils/results.mli @@ -72,8 +72,9 @@ 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 +val expr_deps : Cil_types.exp -> request -> Locations.Zone.t (* The zone of bits read to evaluate the expression, including adresses computation *) +val lval_deps : Cil_types.lval -> request -> Locations.Zone.t (* The zone of bits read to evaluate the lvalue, including lvalue zone itself *) +val address_deps : Cil_types.lval -> request -> Locations.Zone.t (* The zone of bits read to evaluate the lvalue, excluding the lvalue zone itself *) (* Evaluation *) val eval_var : Cil_types.varinfo -> request -> value evaluation