[Gui] fixes frama-c-gui -no-autoload-plugins tests/rte/memaccess.c

src/plugins/gui/property_navigator.ml

@@ -25,8 +25,8 @@ module Rte = struct
     string
     * (Cil_types.kernel_function -> bool -> unit)
     * (Cil_types.kernel_function -> bool)
-  let get_all_status = Extlib.mk_fun "Property_navigator.Rte.get_all_status"
-  let register_get_all_status getter = get_all_status := getter
+  let get_all_status: (unit -> status_accessor list) option ref = ref None
+  let register_get_all_status getter = get_all_status := Some getter
 end
 
 open Design
@@ -229,6 +229,10 @@ struct
     checks := chk :: !checks;
     chk
 
+  let hint_rte hint =
+    if Option.is_some !Rte.get_all_status then hint
+    else hint ^ " (but RteGen plugin is inactive)"
+
   let onlyCurrent = add ~name:"Current function" ~default:false
       ~hint:"Only show properties related to current function" ()
 
@@ -257,7 +261,7 @@ struct
   (* Function called when RTEs are enabled or disabled. *)
   let set_rte = ref (fun _b -> ())
   let rte = add ~set:(fun b -> !set_rte b) ~name:"RTEs"
-      ~hint:"Show runtime errors" ()
+      ~hint:(hint_rte "Show runtime errors") ()
   let invariant = add ~name:"Invariant"
       ~hint:"Show loop invariants" ()
   let variant = add ~name:"Variant"
@@ -282,9 +286,9 @@ struct
       ~hint:"Show 'reachable' hypotheses" ()
 
   let rteNotGenerated = add ~default:false ~name:"Non generated"
-      ~hint:"Show RTEs assertions that remain to generate" ()
+      ~hint:(hint_rte "Show RTEs assertions that remain to generate") ()
   let rteGenerated = add ~default:false ~name:"Generated"
-      ~hint:"Show RTEs assertions that have been generated" ()
+      ~hint:(hint_rte "Show RTEs assertions that have been generated") ()
 
   let valid = add ~name:"Valid"
       ~hint:"Show properties that are proven valid" ()
@@ -714,7 +718,10 @@ let make_panel (main_ui:main_window_extension_points) =
          ) main_ui#file_tree#selected_globals)
     in
 
-    let rte_get_all_statuses = !Rte.get_all_status () in
+    let rte_get_all_statuses = match !Rte.get_all_status with
+      | None -> []
+      | Some registered_getter -> registered_getter ()
+    in
     (* All non-filtered RTE statuses for a given function *)
     let rte_kf kf = List.fold_left (aux_rte kf) [] rte_get_all_statuses in
     (* Add RTE statuses for all functions. We cannot simply iterate over