diff options
| -rw-r--r-- | lib/nostd/sail.h | 2 | ||||
| -rw-r--r-- | src/jib/c_backend.ml | 3 | ||||
| -rw-r--r-- | src/jib/c_backend.mli | 3 | ||||
| -rw-r--r-- | src/sail.ml | 3 |
4 files changed, 9 insertions, 2 deletions
diff --git a/lib/nostd/sail.h b/lib/nostd/sail.h index d553e6b3..be725fbc 100644 --- a/lib/nostd/sail.h +++ b/lib/nostd/sail.h @@ -357,7 +357,7 @@ typedef double real; typedef mpq_t real; #endif -SAIL_BUILTIN_TYPE(real); +SAIL_BUILTIN_TYPE(real) void CREATE_OF(real, sail_string)(real *rop, const sail_string op); void CONVERT_OF(real, sail_string)(real *rop, const sail_string op); 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 diff --git a/src/sail.ml b/src/sail.ml index 2f16f130..81683b4d 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -180,6 +180,9 @@ let options = Arg.align ([ ( "-c_no_rts", Arg.Set C_backend.opt_no_rts, " do not include the Sail runtime" ); + ( "-c_no_lib", + Arg.Tuple [Arg.Set C_backend.opt_no_lib; Arg.Set C_backend.opt_no_rts], + " do not include the Sail runtime or library" ); ( "-c_prefix", Arg.String (fun prefix -> C_backend.opt_prefix := prefix), "<prefix> prefix generated C functions" ); |