diff options
| author | Robert Norton | 2018-06-28 14:18:16 +0100 |
|---|---|---|
| committer | Robert Norton | 2018-06-28 14:18:22 +0100 |
| commit | 28b054b28a5dc32bb927e7093690f4fe74d65426 (patch) | |
| tree | d590244e085af353ce20c57b53f8a40698350053 /src | |
| parent | 48c36bf2378ed551d3fcf9d5eda2995ce1dad226 (diff) | |
Add option to build ocaml with bisect_ppx coverage support. Add cheri targets using this.
Diffstat (limited to 'src')
| -rw-r--r-- | src/ocaml_backend.ml | 11 | ||||
| -rw-r--r-- | src/sail.ml | 4 |
2 files changed, 12 insertions, 3 deletions
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 369a325c..5ffb1647 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -60,6 +60,7 @@ module Big_int = Nat_big_num let opt_trace_ocaml = ref false (* Option to not build generated ocaml by default *) let opt_ocaml_nobuild = ref false +let opt_ocaml_coverage = ref false type ctx = { register_inits : tannot exp list; @@ -704,8 +705,11 @@ let ocaml_compile spec defs = let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/elf_loader.ml .") in let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/sail_lib.ml .") in let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/util.ml .") in - let _ = Unix.system ("cp -r " ^ sail_dir ^ "/lib/_tags .") in + let tags_file = if !opt_ocaml_coverage then "_tags_coverage" else "_tags" in + let _ = Unix.system ("cp -r " ^ sail_dir ^ "/lib/" ^ tags_file ^ " _tags") in let out_chan = open_out (spec ^ ".ml") in + if !opt_ocaml_coverage then + ignore(Unix.system ("cp -r " ^ sail_dir ^ "/lib/myocamlbuild_coverage.ml myocamlbuild.ml")); ocaml_pp_defs out_chan defs; close_out out_chan; if IdSet.mem (mk_id "main") (Initial_check.val_spec_ids defs) @@ -716,7 +720,10 @@ let ocaml_compile spec defs = output_string out_chan (ocaml_main spec sail_dir); close_out out_chan; if not !opt_ocaml_nobuild then ( - system_checked "ocamlbuild -use-ocamlfind main.native"; + if !opt_ocaml_coverage then + system_checked "BISECT_COVERAGE=YES ocamlbuild -use-ocamlfind -plugin-tag 'package(bisect_ppx-ocamlbuild)' main.native" + else + system_checked "ocamlbuild -use-ocamlfind main.native"; ignore (Unix.system ("cp main.native " ^ cwd ^ "/" ^ spec)) ) end diff --git a/src/sail.ml b/src/sail.ml index a933ce59..046445d1 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -62,7 +62,6 @@ let opt_print_verbose = ref false let opt_print_lem_ast = ref false let opt_print_lem = ref false let opt_print_ocaml = ref false -let opt_ocaml_nobuild = ref false let opt_print_c = ref false let opt_print_latex = ref false let opt_print_coq = ref false @@ -97,6 +96,9 @@ let options = Arg.align ([ ( "-ocaml_trace", Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen; Arg.Set Ocaml_backend.opt_trace_ocaml], " output an OCaml translated version of the input with tracing instrumentation, implies -ocaml"); + ( "-ocaml-coverage", + Arg.Set Ocaml_backend.opt_ocaml_coverage, + "Build ocaml with bisect_ppx coverage reporting (requires opam packages bisect_ppx-ocamlbuild and bisect_ppx)."); ( "-latex", Arg.Set opt_print_latex, " pretty print the input to latex"); |