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