diff options
| author | Alasdair | 2018-07-08 14:19:23 +0100 |
|---|---|---|
| committer | Alasdair | 2018-07-08 14:19:23 +0100 |
| commit | 8286993fe02b151dc1daa808b422f1ba97e05602 (patch) | |
| tree | c68ee5c4e67866ae58eb99c88a423eaf89b02c98 /src | |
| parent | d819af50c403935cb6825afa914e03c816e156cb (diff) | |
Add -static flag that controls whether generated C functions are static
By default generated functions are non-static, using the -static flag makes them static which is useful for measuring coverage using generated code. Some utility helper functions will always be static, but the compiled versions of sail functions won't be unless this flag is set.
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"); |