From 072ad968b4e1b970f4d9c67e24b6647d46cb79df Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 30 Nov 2021 14:26:19 +0100
Subject: [PATCH] [kernel] add test case for orphan emitter
---
tests/misc/oracle/orphan_emitter.res.oracle | 2 ++
tests/misc/oracle/orphan_emitter_sav.err | 0
tests/misc/oracle/orphan_emitter_sav.res | 1 +
tests/misc/orphan_emitter.i | 12 ++++++++++++
tests/misc/orphan_emitter.ml | 21 +++++++++++++++++++++
5 files changed, 36 insertions(+)
create mode 100644 tests/misc/oracle/orphan_emitter.res.oracle
create mode 100644 tests/misc/oracle/orphan_emitter_sav.err
create mode 100644 tests/misc/oracle/orphan_emitter_sav.res
create mode 100644 tests/misc/orphan_emitter.i
create mode 100644 tests/misc/orphan_emitter.ml
diff --git a/tests/misc/oracle/orphan_emitter.res.oracle b/tests/misc/oracle/orphan_emitter.res.oracle
new file mode 100644
index 00000000000..b4a4e9e9636
--- /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 00000000000..e69de29bb2d
diff --git a/tests/misc/oracle/orphan_emitter_sav.res b/tests/misc/oracle/orphan_emitter_sav.res
new file mode 100644
index 00000000000..8a5aa9b933f
--- /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 00000000000..43b7d53e648
--- /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 00000000000..573894ba52e
--- /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
--
GitLab