Merge branch 'fix/kernel/orphan-emitter' into 'master'

[kernel] Usable_emitter.get returns [orphan] when the emitter does not exists.

See merge request frama-c/frama-c!3457

src/kernel_services/ast_data/annotations.ml

@@ -365,14 +365,7 @@ let code_annot_emitter ?filter stmt =
   try
     let tbl = Code_annots.find stmt in
     let filter e l acc =
-      let e =
-        try Emitter.Usable_emitter.get e
-        with Not_found ->
-          (* in some cases, e.g. when loading a state with a different set
-             of plugins loaded, the original emitter might not be available,
-             leading to discarding annotations. Let the kernel adopt them. *)
-          Emitter.orphan
-      in
+      let e = Emitter.Usable_emitter.get e in
       match filter with
       | None -> List.map (fun a -> a, e) l @ acc
       | Some f ->

src/kernel_services/plugin_entry_points/emitter.ml

@@ -23,10 +23,6 @@
 (* Modules [Hashtbl] and [Kernel] are not usable here. Thus use above modules
    instead. *)
 
-(**************************************************************************)
-(** {2 Datatype} *)
-(**************************************************************************)
-
 type kind = Property_status | Alarm | Code_annot | Funspec | Global_annot
 
 type emitter =
@@ -35,6 +31,59 @@ type emitter =
     tuning_parameters: Typed_parameter.t list;
     correctness_parameters: Typed_parameter.t list }
 
+(**************************************************************************)
+(** {2 Implementation for Plug-in Developers} *)
+(**************************************************************************)
+
+let names: unit Datatype.String.Hashtbl.t = Datatype.String.Hashtbl.create 7
+
+let create name kinds ~correctness ~tuning =
+  if Datatype.String.Hashtbl.mem names name then
+    Kernel.fatal "emitter %s already exists with the same parameters" name;
+  let e =
+    { name = name;
+      kinds = kinds;
+      correctness_parameters = correctness;
+      tuning_parameters = tuning }
+  in
+  Datatype.String.Hashtbl.add names name ();
+  e
+
+let dummy = create "dummy" [] ~correctness:[] ~tuning:[]
+
+let get_name e = e.name
+
+let correctness_parameters e =
+  List.map (fun p -> p.Typed_parameter.name) e.correctness_parameters
+
+let tuning_parameters e =
+  List.map (fun p -> p.Typed_parameter.name) e.tuning_parameters
+
+let end_user =
+  create
+    "End-User"
+    [ Property_status; Code_annot; Funspec; Global_annot ]
+    ~correctness:[]
+    ~tuning:[]
+
+let kernel =
+  create
+    "Frama-C kernel"
+    [ Property_status; Funspec ]
+    ~correctness:[]
+    ~tuning:[]
+
+let orphan =
+  create
+    "Orphan"
+    [ Code_annot; Funspec; Global_annot ]
+    ~correctness:[]
+    ~tuning:[]
+
+(**************************************************************************)
+(** {2 Datatype} *)
+(**************************************************************************)
+
 module D =
   Datatype.Make_with_collections
     (struct
@@ -106,7 +155,7 @@ module Usable_emitter = struct
         let mem_project = Datatype.never_any_project
       end)
 
-  let get e =
+  let unsafe_get e =
     let get_params map =
       Datatype.String.Map.fold
         (fun s _ acc -> Typed_parameter.get s :: acc)
@@ -118,6 +167,13 @@ module Usable_emitter = struct
       correctness_parameters = get_params e.correctness_values;
       tuning_parameters = get_params e.tuning_values }
 
+  (* In some cases, e.g. when loading a state with a different set
+     of plugins loaded, the original emitter might not be available,
+     leading to discarding annotations. Let the kernel adopt them. *)
+  let get e =
+    try unsafe_get e
+    with Not_found -> orphan
+
   let get_name e = e.u_name
   let get_unique_name e = Format.asprintf "%a" pretty e
 
@@ -134,55 +190,6 @@ module Usable_emitter = struct
 
 end
 
-(**************************************************************************)
-(** {2 Implementation for Plug-in Developers} *)
-(**************************************************************************)
-
-let names: unit Datatype.String.Hashtbl.t = Datatype.String.Hashtbl.create 7
-
-let create name kinds ~correctness ~tuning =
-  if Datatype.String.Hashtbl.mem names name then
-    Kernel.fatal "emitter %s already exists with the same parameters" name;
-  let e =
-    { name = name;
-      kinds = kinds;
-      correctness_parameters = correctness;
-      tuning_parameters = tuning }
-  in
-  Datatype.String.Hashtbl.add names name ();
-  e
-
-let dummy = create "dummy" [] ~correctness:[] ~tuning:[]
-
-let get_name e = e.name
-
-let correctness_parameters e =
-  List.map (fun p -> p.Typed_parameter.name) e.correctness_parameters
-
-let tuning_parameters e =
-  List.map (fun p -> p.Typed_parameter.name) e.tuning_parameters
-
-let end_user =
-  create
-    "End-User"
-    [ Property_status; Code_annot; Funspec; Global_annot ]
-    ~correctness:[]
-    ~tuning:[]
-
-let kernel =
-  create
-    "Frama-C kernel"
-    [ Property_status; Funspec ]
-    ~correctness:[]
-    ~tuning:[]
-
-let orphan =
-  create
-    "Orphan"
-    [ Code_annot; Funspec; Global_annot ]
-    ~correctness:[]
-    ~tuning:[]
-
 (**************************************************************************)
 (** {2 State of all known emitters} *)
 (**************************************************************************)

tests/misc/oracle/orphan_emitter.res.oracle

+[kernel] Warning: emitter emitter1: correctness parameter -orphan does not exist anymore. Ignored.
+[kernel] Warning: 11 states in saved file ignored. They are invalid in this Frama-C configuration.

tests/misc/oracle/orphan_emitter_sav.res

+[kernel] Parsing orphan_emitter.i (no preprocessing)

tests/misc/orphan_emitter.i

+/* run.config
+ PLUGIN: @EVA_PLUGINS@
+ MODULE: @PTEST_NAME@
+   EXECNOW: BIN @PTEST_NAME@.sav LOG @PTEST_NAME@_sav.res LOG @PTEST_NAME@_sav.err @frama-c@ @PTEST_FILE@ -save @PTEST_NAME@.sav > @PTEST_NAME@_sav.res 2> @PTEST_NAME@_sav.err
+ MODULE:
+ COMMENT: the CMD line below omits @PTEST_FILE@ on purpose (due to -load)
+ CMD: @frama-c@ @PTEST_OPTIONS@
+   OPT: -load %{dep:@PTEST_NAME@.sav} -eva -eva-verbose 0
+*/
+int main() {
+  return 0;
+}

tests/misc/orphan_emitter.ml

+module P =
+  Plugin.Register
+    (struct
+      let name = "Orphan"
+      let shortname = "orphan"
+      let help = ""
+     end)
+
+module S =
+  P.True(struct let option_name = "-orphan" let help = "" end)
+
+let emitter1 =
+  Emitter.create "emitter1" [ Emitter.Code_annot ]
+    ~correctness:[ S.parameter ] ~tuning:[]
+
+let main () =
+  let kf = Globals.Functions.find_by_name "main" in
+  let stmt = Kernel_function.find_first_stmt kf in
+  Annotations.add_assert emitter1 stmt Logic_const.ptrue
+
+let () = Db.Main.extend main