diff options
Diffstat (limited to 'src/jib')
| -rw-r--r-- | src/jib/c_backend.ml | 3 | ||||
| -rw-r--r-- | src/jib/c_backend.mli | 3 |
2 files changed, 5 insertions, 1 deletions
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 4f0770ff..3814b864 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -66,6 +66,7 @@ let c_verbosity = ref 0 let opt_static = ref false let opt_no_main = ref false let opt_memo_cache = ref false +let opt_no_lib = ref false let opt_no_rts = ref false let opt_prefix = ref "z" let opt_extra_params = ref None @@ -2182,7 +2183,7 @@ let compile_ast env output_chan c_includes ast = let docs = separate_map (hardline ^^ hardline) (codegen_def ctx) cdefs in let preamble = separate hardline - ([ string "#include \"sail.h\"" ] + ((if !opt_no_lib then [] else [string "#include \"sail.h\""]) @ (if !opt_no_rts then [] else [ string "#include \"rts.h\""; string "#include \"elf.h\"" ]) diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli index 90e86d70..2f748fd7 100644 --- a/src/jib/c_backend.mli +++ b/src/jib/c_backend.mli @@ -64,6 +64,9 @@ val opt_no_main : bool ref before executing any instruction semantics. *) val opt_no_rts : bool ref +(** Do not include sail.h by default *) +val opt_no_lib : bool ref + (** Ordinarily we use plain z-encoding to name-mangle generated Sail identifiers into a form suitable for C. If opt_prefix is set, then the "z" which is added on the front of each generated C function |