[kernel] fix issue in emitter filtering when emitter is not usable

When loading some state, it may happen that some annotations are found to have
been emitted by emitters that are no longer usable. This commit let the kernel
adopt them, keeping them available as was the case before refactoring
`Annotations.code_annot` to use `Annotations.code_annot_emitter`.

src/kernel_services/ast_data/annotations.ml

@@ -352,7 +352,14 @@ let code_annot_emitter ?filter stmt =
   try
     let tbl = Code_annots.find stmt in
     let filter e l acc =
-      let e = Emitter.Usable_emitter.get e in
+      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.kernel
+      in
       match filter with
       | None -> List.map (fun a -> a, e) l @ acc
       | Some f ->

tests/misc/my_visitor.c

 /* run.config
 EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
 EXECNOW: LOG my_visitor_sav.res LOG my_visitor_sav.err BIN my_visitor.sav FRAMAC_PLUGIN=./lib/plugins @frama-c@ @PTEST_FILE@ -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -main f -save @PTEST_DIR@/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@_sav.res 2> @PTEST_DIR@/result/@PTEST_NAME@_sav.err
-OPT: -load @PTEST_DIR@/@PTEST_NAME@.sav -print
+OPT: -load @PTEST_DIR@/@PTEST_NAME@.sav -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -no-my-visitor -print
+OPT: -load @PTEST_DIR@/@PTEST_NAME@.sav -no-autoload-plugins -print
 */
 int f() {
   int y = 0;

tests/misc/my_visitor.ml

@@ -16,6 +16,9 @@ module S =
 module S2 =
   P.False(struct let option_name = "-s2" let help = "" end)
 
+module Enabled =
+  P.True(struct let option_name = "-my-visitor" let help = "" end)
+
 let emitter1 = 
   Emitter.create "emitter1" [ Emitter.Code_annot ]
     ~correctness:[ S.parameter ] ~tuning:[]
@@ -64,28 +67,32 @@ let print () =
   Kernel.log "================================"
 
 let main () =
-  (* The initial AST *)
-  print ();
-  let file = Ast.get () in
-  ignore (Cil.visitCilFileSameGlobals (new foo:>cilVisitor) file);
-  (* The AST with all asserts *)
-  print ();
-  Kernel.SafeArrays.set false;
-  Project.clear 
-    ~selection:(State_selection.Static.with_dependencies S.self) ();
-  (* The AST with 1/2 asserts *)
-  print ()
+  if Enabled.get() then begin
+    (* The initial AST *)
+    print ();
+    let file = Ast.get () in
+    ignore (Cil.visitCilFileSameGlobals (new foo:>cilVisitor) file);
+    (* The AST with all asserts *)
+    print ();
+    Kernel.SafeArrays.set false;
+    Project.clear
+      ~selection:(State_selection.Static.with_dependencies S.self) ();
+    (* The AST with 1/2 asserts *)
+    print ()
+  end
 
 let () = Db.Main.extend main
 
 (* This other main is a simple test for deep copy. *)
 
 let main () =
-  let p = File.create_project_from_visitor "param" (new Visitor.frama_c_copy) in
-  let selection = State_selection.singleton Kernel.LibEntry.self in
-  Project.copy ~selection p;
-  Kernel.LibEntry.on ();
-  assert (Kernel.LibEntry.get ());
-  assert (Project.on p ~selection (fun () -> not (Kernel.LibEntry.get ())) ())
+  if Enabled.get() then begin
+    let p = File.create_project_from_visitor "param" (new Visitor.frama_c_copy) in
+    let selection = State_selection.singleton Kernel.LibEntry.self in
+    Project.copy ~selection p;
+    Kernel.LibEntry.on ();
+    assert (Kernel.LibEntry.get ());
+    assert (Project.on p ~selection (fun () -> not (Kernel.LibEntry.get ())) ())
+  end
 
 let () = Db.Main.extend main

tests/misc/oracle/my_visitor.0.res.oracle

+[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
+/* Generated by Frama-C */
+int f(void)
+{
+  int __retres;
+  /*@ assert emitter2: ∀ ℤ x; x ≡ x; */
+  int y = 0;
+  y ++;
+  /*@ assert y ≡ 1; */
+  /*@ assert emitter2: ∀ ℤ x; x ≡ x; */
+  ;
+  __retres = 0;
+  /*@ assert emitter2: ∀ ℤ x; x ≡ x; */
+  return __retres;
+}
+
+

tests/misc/oracle/my_visitor.1.res.oracle

+[kernel] Warning: emitter emitter1: correctness parameter -s does not exist anymore. Ignored.
+[kernel] Warning: emitter emitter2: correctness parameter -s2 does not exist anymore. Ignored.
+[kernel] Warning: 15 states in saved file ignored. They are invalid in this Frama-C configuration.
+[kernel] Warning: emitter emitter1: correctness parameter -s does not exist anymore. Ignored.
+[kernel] Warning: emitter emitter2: correctness parameter -s2 does not exist anymore. Ignored.
+[kernel] Warning: 15 states in saved file ignored. They are invalid in this Frama-C configuration.
+[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
+/* Generated by Frama-C */
+int f(void)
+{
+  int __retres;
+  /*@ assert emitter2: ∀ ℤ x; x ≡ x; */
+  int y = 0;
+  y ++;
+  /*@ assert y ≡ 1; */
+  /*@ assert emitter2: ∀ ℤ x; x ≡ x; */
+  ;
+  __retres = 0;
+  /*@ assert emitter2: ∀ ℤ x; x ≡ x; */
+  return __retres;
+}
+
+