diff options
| -rw-r--r-- | src/process_file.ml | 3 | ||||
| -rw-r--r-- | src/process_file.mli | 1 | ||||
| -rw-r--r-- | src/sail.ml | 14 |
3 files changed, 18 insertions, 0 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index 170a544a..d239b0c0 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -99,6 +99,9 @@ let default_symbols = let symbols = ref default_symbols +let have_symbol symbol = + StringSet.mem symbol !symbols + let clear_symbols () = symbols := default_symbols let cond_pragma l defs = diff --git a/src/process_file.mli b/src/process_file.mli index 91cde014..55c7906b 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -53,6 +53,7 @@ val parse_file : ?loc:Parse_ast.l -> string -> Parse_ast.defs val clear_symbols : unit -> unit +val have_symbol : string -> bool val preprocess_ast : (Arg.key * Arg.spec * Arg.doc) list -> Parse_ast.defs -> Parse_ast.defs val check_ast : Type_check.Env.t -> unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t diff --git a/src/sail.ml b/src/sail.ml index e9b1914d..b15e1746 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -70,6 +70,7 @@ let opt_file_arguments = ref ([]:string list) let opt_process_elf : string option ref = ref None let opt_ocaml_generators = ref ([]:string list) let opt_splice = ref ([]:string list) +let opt_have_feature = ref None let set_target name = Arg.Unit (fun _ -> opt_target := Some name) @@ -276,6 +277,9 @@ let options = Arg.align ([ ( "-memo", Arg.Tuple [Arg.Set opt_memo_z3; Arg.Set C_backend.opt_memo_cache], " memoize calls to z3, and intermediate compilation results"); + ( "-have_feature", + Arg.String (fun symbol -> opt_have_feature := Some symbol), + " check if a feature symbol is set by default"); ( "-splice", Arg.String (fun s -> opt_splice := s :: !opt_splice), "<filename> add functions from file, replacing existing definitions where necessary"); @@ -545,7 +549,17 @@ let target name out_name ast type_envs = | Some t -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ ("Undefined target: " ^ t)) +let feature_check () = + match !opt_have_feature with + | None -> () + | Some symbol -> + if Process_file.have_symbol symbol then + exit 0 + else + exit 2 + let main () = + feature_check (); if !opt_print_version then print_endline version else |