[Studia] Use the new Eva API

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

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
 

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"

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}