diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml index 616667b0f30afa0f4297c205efddfe5fbe370e1c..1eb538ec66dfeaa62afa13d4effc00829a6bd968 100644 --- a/src/kernel_services/ast_data/annotations.ml +++ b/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 -> diff --git a/tests/misc/my_visitor.c b/tests/misc/my_visitor.c index 29355fd152e80c899adebc677eb1abba062d46d5..9ce70834706be3ccc9798f57e77d6e9e52258308 100644 --- a/tests/misc/my_visitor.c +++ b/tests/misc/my_visitor.c @@ -1,7 +1,8 @@ /* 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; diff --git a/tests/misc/my_visitor.ml b/tests/misc/my_visitor.ml index 4e2a100c4cb28ba7ef9e9b08b645a6e5e3634618..09545f270ae554bcbfd5e1120ce60e7cc051fa12 100644 --- a/tests/misc/my_visitor.ml +++ b/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 diff --git a/tests/misc/oracle/my_visitor.0.res.oracle b/tests/misc/oracle/my_visitor.0.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..757a20ca369650eea0ce2c3162081003a9e5dc0d --- /dev/null +++ b/tests/misc/oracle/my_visitor.0.res.oracle @@ -0,0 +1,17 @@ +[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; +} + + diff --git a/tests/misc/oracle/my_visitor.1.res.oracle b/tests/misc/oracle/my_visitor.1.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..14717c12726eef25759c4b1f52744367b6b3fe94 --- /dev/null +++ b/tests/misc/oracle/my_visitor.1.res.oracle @@ -0,0 +1,23 @@ +[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; +} + +