Skip to content
Snippets Groups Projects
Commit 072ad968 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[kernel] add test case for orphan emitter

parent 274827cc
No related branches found
No related tags found
No related merge requests found
[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.
[kernel] Parsing orphan_emitter.i (no preprocessing)
/* 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;
}
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
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment