diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-21 22:42:32 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-21 22:42:32 +0200 |
| commit | 25547c7d1f6a0fb75ff1d8e7287d9305e0dbf293 (patch) | |
| tree | 22e72881226f3a5661f335605e99d6243bf39f41 /tools | |
| parent | 1bd4d678fb719a6a52ade232eb2b36a6e621677a (diff) | |
| download | compcert-kvx-25547c7d1f6a0fb75ff1d8e7287d9305e0dbf293.tar.gz compcert-kvx-25547c7d1f6a0fb75ff1d8e7287d9305e0dbf293.zip | |
generate mkpass
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/compiler_expand.ml | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index 7ca3c755..1ef233e7 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -53,7 +53,17 @@ let print_rtl_transf oc = Printf.fprintf oc "%s.transf_program)\n" pass_name; Printf.fprintf oc " @@ print (print_RTL %d)\n" (succ i) ) rtl_passes;; - + +let print_rtl_mkpass oc = + Array.iter (fun (partial, trigger, time_label, pass_name) -> + output_string oc " ::: mkpass ("; + (match trigger with + | Always -> () + | Option s -> + Printf.fprintf oc "match_if Compopts.%s " s); + Printf.fprintf oc "%sproof.match_prog)\n" pass_name) + rtl_passes;; + if (Array.length Sys.argv)<>3 then exit 1;; @@ -69,6 +79,8 @@ let filename_in = Sys.argv.(1) and filename_out = Sys.argv.(2) in print_rtl_require oc | "EXPAND_RTL_REQUIRE_PROOF" -> print_rtl_require_proof oc + | "EXPAND_RTL_MKPASS" -> + print_rtl_mkpass oc | line -> (output_string oc line; output_char oc '\n') done |