From 1719c9ded4d02889f44944f70d3d32512c5a539c Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 11 Jun 2020 15:30:04 +0200
Subject: [PATCH] [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 | 9 ++++-
tests/misc/my_visitor.c | 3 +-
tests/misc/my_visitor.ml | 41 ++++++++++++---------
tests/misc/oracle/my_visitor.0.res.oracle | 17 +++++++++
tests/misc/oracle/my_visitor.1.res.oracle | 23 ++++++++++++
5 files changed, 74 insertions(+), 19 deletions(-)
create mode 100644 tests/misc/oracle/my_visitor.0.res.oracle
create mode 100644 tests/misc/oracle/my_visitor.1.res.oracle
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index 616667b0f30..1eb538ec66d 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 29355fd152e..9ce70834706 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 4e2a100c4cb..09545f270ae 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 00000000000..757a20ca369
--- /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 00000000000..14717c12726
--- /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;
+}
+
+
--
GitLab