diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index 8869fe97088901d6ae11313b3bb9cb474203aec4..56739c79dd7706fde593cbef832fe22275d1d18c 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/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 ->
diff --git a/src/kernel_services/plugin_entry_points/emitter.ml b/src/kernel_services/plugin_entry_points/emitter.ml
index d44861ba06cd48b63905c295e0fa67284b34b33c..9f5ada97cc5e2a407f0dd6ea0b06003a43b9a9d9 100644
--- a/src/kernel_services/plugin_entry_points/emitter.ml
+++ b/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} *)
(**************************************************************************)
diff --git a/tests/misc/oracle/orphan_emitter.res.oracle b/tests/misc/oracle/orphan_emitter.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b4a4e9e9636b1ef49df2c0fd7a6aaf94a196a565
--- /dev/null
+++ b/tests/misc/oracle/orphan_emitter.res.oracle
@@ -0,0 +1,2 @@
+[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.
diff --git a/tests/misc/oracle/orphan_emitter_sav.err b/tests/misc/oracle/orphan_emitter_sav.err
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/misc/oracle/orphan_emitter_sav.res b/tests/misc/oracle/orphan_emitter_sav.res
new file mode 100644
index 0000000000000000000000000000000000000000..8a5aa9b933fce678411ffde32a3361b0f2f4ce08
--- /dev/null
+++ b/tests/misc/oracle/orphan_emitter_sav.res
@@ -0,0 +1 @@
+[kernel] Parsing orphan_emitter.i (no preprocessing)
diff --git a/tests/misc/orphan_emitter.i b/tests/misc/orphan_emitter.i
new file mode 100644
index 0000000000000000000000000000000000000000..43b7d53e648cbfb3063b93f83cae64e896ac15ab
--- /dev/null
+++ b/tests/misc/orphan_emitter.i
@@ -0,0 +1,12 @@
+/* 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;
+}
diff --git a/tests/misc/orphan_emitter.ml b/tests/misc/orphan_emitter.ml
new file mode 100644
index 0000000000000000000000000000000000000000..573894ba52e7d833dad60df9e527c724769e1e63
--- /dev/null
+++ b/tests/misc/orphan_emitter.ml
@@ -0,0 +1,21 @@
+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