diff --git a/src/plugins/studia/reads.ml b/src/plugins/studia/reads.ml index 3685d8cba7b689b4e0ee46f1408db61985065d61..0a432ee23a669275b49c37bbc8324b1974c869c3 100644 --- a/src/plugins/studia/reads.ml +++ b/src/plugins/studia/reads.ml @@ -44,15 +44,13 @@ class find_read zlval = object let deps = match lvopt with | None -> deps | Some lv -> - let dlv, _ = - !Db.Value.lval_to_loc_with_deps (Kstmt stmt) ~deps:Zone.bottom lv - in + let dlv = Eva.Results.(before stmt |> address_deps lv) in Zone.join dlv deps in let direct = Zone.intersects deps zlval in (* now determine if the functions called at [stmt] read directly or indirectly [zlval] *) - let aux_kf kf effects = + let aux_kf effects kf = let inputs = !Db.Inputs.get_internal kf in (* TODO: change to this once we can get "full" inputs through Inout. Currently, non operational inputs disappear, and this function @@ -68,9 +66,9 @@ class find_read zlval = object else effects (* this function pointer does not read [zlval] *) in - let kfs = Db.Value.call_to_kernel_function stmt in + let kfs = Eva.Results.callee stmt in let effects = - Kernel_function.Hptset.fold aux_kf kfs {direct; indirect = false} + List.fold_left aux_kf {direct; indirect = false} kfs in res <- (stmt, effects) :: res end diff --git a/src/plugins/studia/studia_gui.ml b/src/plugins/studia/studia_gui.ml index 9008db351027fc01dcfd385aba799782e8a4f718..c7b1425c394d7c776424631c55b840ec99640425 100644 --- a/src/plugins/studia/studia_gui.ml +++ b/src/plugins/studia/studia_gui.ml @@ -90,7 +90,7 @@ struct (Stmt.Map.Make(Datatype.String.Set)) (struct let name = Info.name - let dependencies = [ Db.Value.self ] + let dependencies = [ Eva.Analysis.self ] let default () = Stmt.Map.empty end) @@ -184,7 +184,7 @@ module StudiaState = (Stmt) (struct let name = "Studia.Highlighter.StudiaState" - let dependencies = [ Db.Value.self ] + let dependencies = [ Eva.Analysis.self ] end) let reset () = @@ -226,7 +226,7 @@ let highlighter (buffer:Design.reactive_buffer) localizable ~start ~stop = with Not_found -> () let check_value (main_ui:Design.main_window_extension_points) = - Db.Value.is_computed () || + Eva.Analysis.is_computed () || let answer = GToolbox.question_box ~title:("Eva Needed") ~buttons:[ "Run"; "Cancel" ] @@ -234,7 +234,7 @@ let check_value (main_ui:Design.main_window_extension_points) = ^"Do you want to run Eva now ?") in answer = 1 && - match main_ui#full_protect ~cancelable:true !Db.Value.compute with + match main_ui#full_protect ~cancelable:true Eva.Analysis.compute with | Some _ -> true | None -> false diff --git a/src/plugins/studia/studia_request.ml b/src/plugins/studia/studia_request.ml index ff3f94c3d1061bc178020507cb565241d5cb20dc..f1a94a67bd23fcdd8d289fa96ff300961348781d 100644 --- a/src/plugins/studia/studia_request.ml +++ b/src/plugins/studia/studia_request.ml @@ -81,7 +81,10 @@ let compute kind zone = let empty = { direct = []; indirect = []; } in List.fold_left add empty stmts -let lval_location kinstr lval = !Db.Value.lval_to_zone kinstr lval +let lval_location kinstr lval = + Eva.Results.( + before_kinstr kinstr |> eval_address lval |> as_zone |> + default Locations.Zone.bottom) let () = Request.register ~package ~kind:`GET ~name:"getReadsLval" diff --git a/src/plugins/studia/writes.ml b/src/plugins/studia/writes.ml index fa29b18e974c25b9234fa1e95b11f4f3fd8005aa..d323327d03be5af511b1e409e4e2acaeedaa294e 100644 --- a/src/plugins/studia/writes.ml +++ b/src/plugins/studia/writes.ml @@ -35,7 +35,7 @@ type effects = { (** Does the functions called at [stmt] modify directly or indirectly [zlval] *) let effects_of_call stmt zlval effects = - let aux_kf kf effects = + let aux_kf effects kf = let inout = !Db.Operational_inputs.get_internal_precise ~stmt kf in let out = inout.Inout_type.over_outputs in if Zone.intersects out zlval then @@ -47,8 +47,8 @@ let effects_of_call stmt zlval effects = else effects in - let kfs = Db.Value.call_to_kernel_function stmt in - Kernel_function.Hptset.fold aux_kf kfs effects + let kfs = Eva.Results.callee stmt in + List.fold_left aux_kf effects kfs class find_write zlval = object (self) inherit Visitor.frama_c_inplace @@ -66,8 +66,8 @@ class find_write zlval = object (self) let direct_write = match lvopt with | None -> false | Some lv -> - let zlv = !Db.Value.lval_to_zone (Kstmt stmt) lv in - Zone.intersects zlv zlval + Eva.Results.(before stmt |> eval_address lv |> as_zone) |> + Result.fold ~ok:(Zone.intersects zlval) ~error:(fun _ -> false) in let effects = effects_of_call stmt zlval {direct = direct_write; indirect =false}