diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/c_backend.ml | 7 | ||||
| -rw-r--r-- | src/sail.ml | 3 |
2 files changed, 8 insertions, 2 deletions
diff --git a/src/c_backend.ml b/src/c_backend.ml index 09501ce9..e92ca1a6 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -63,6 +63,7 @@ module Big_int = Nat_big_num let c_verbosity = ref 0 let opt_ddump_flow_graphs = ref false let opt_trace = ref false +let opt_static = ref false (* Optimization flags *) let optimize_primops = ref false @@ -2547,10 +2548,12 @@ let codegen_def' ctx = function match ret_arg with | None -> assert (is_stack_ctyp ret_ctyp); - string "static " ^^ string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_id id ^^ parens (string args) ^^ hardline + (if !opt_static then string "static " else empty) + ^^ string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_id id ^^ parens (string args) ^^ hardline | Some gs -> assert (not (is_stack_ctyp ret_ctyp)); - string "static void" ^^ space ^^ codegen_id id + (if !opt_static then string "static " else empty) + ^^ string "void" ^^ space ^^ codegen_id id ^^ parens (string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args) ^^ hardline in diff --git a/src/sail.ml b/src/sail.ml index 046445d1..64e60c23 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -121,6 +121,9 @@ let options = Arg.align ([ ( "-Oconstant_fold", Arg.Set Constant_fold.optimize_constant_fold, " Apply constant folding optimizations"); + ( "-static", + Arg.Set C_backend.opt_static, + " Make generated C functions static"); ( "-trace", Arg.Tuple [Arg.Set C_backend.opt_trace; Arg.Set Ocaml_backend.opt_trace_ocaml], " Instrument ouput with tracing"); |