diff --git a/src/plugins/inout/derefs.ml b/src/plugins/inout/derefs.ml index 19bba4c86cccbfb4e72afb0a15313f0db8239d84..53bf4d9d7fa06d2c3c57adc9c83a48294bd6144e 100644 --- a/src/plugins/inout/derefs.ml +++ b/src/plugins/inout/derefs.ml @@ -86,7 +86,7 @@ module Externals = let get_external = Externals.memo (fun kf -> - !Db.Value.compute (); + Eva.Analysis.compute (); if Kernel_function.is_definition kf then try externalize diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml index 43736a78c9436ab1209a6d1bd9af3bed5476bfe3..a21577b15097c2a7897aa580cf72687b3c0f63de 100644 --- a/src/plugins/inout/operational_inputs.ml +++ b/src/plugins/inout/operational_inputs.ml @@ -807,7 +807,7 @@ end let get_internal = Internals.memo (fun kf -> - !Db.Value.compute (); + Eva.Analysis.compute (); try Internals.find kf (* The results may have been computed by the call to Value.compute *) with diff --git a/src/plugins/inout/outputs.ml b/src/plugins/inout/outputs.ml index 1137bece59862b3720436f2da090395382a8cc9e..f7bec37f39e3be3928d06129200804beaf5c6fd2 100644 --- a/src/plugins/inout/outputs.ml +++ b/src/plugins/inout/outputs.ml @@ -48,12 +48,11 @@ class virtual do_it_ = object(self) (* For local initializations, counts the written variable as an output of the function, even if it is const; thus, [for_writing] is false in this case. *) method private do_assign ~for_writing lv = - let state = Db.Value.get_state self#current_kinstr in - let _deps, bits_loc, _exact = - !Db.Value.lval_to_zone_with_deps_state state - ~deps:None ~for_writing lv - in - self#join bits_loc + let access = if for_writing then Write else Read in + let bits_loc = Eva.Results.( + before_kinstr self#current_kinstr |> eval_address lv |> + as_zone ~access) in + Result.iter self#join bits_loc method! vinst i = if Db.Value.is_reachable (Db.Value.noassert_get_state self#current_kinstr) diff --git a/src/plugins/inout/register.ml b/src/plugins/inout/register.ml index f8615a255af358297d2005df233cabb149b43e94..00ca70a65a077cf27bdc6ef4ab6a1d6386517c7d 100644 --- a/src/plugins/inout/register.ml +++ b/src/plugins/inout/register.ml @@ -49,7 +49,7 @@ let main () = Inout_parameters.Output.get () && ShouldOutput.get () then begin ShouldOutput.set false; - !Db.Value.compute (); + Eva.Analysis.compute (); Callgraph.Uses.iter_in_rev_order (fun kf -> if Kernel_function.is_definition kf && !Db.Value.is_called kf