diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/jib/c_backend.ml | 2 | ||||
| -rw-r--r-- | src/sail.ml | 3 |
2 files changed, 4 insertions, 1 deletions
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 27bab7e4..1b949a20 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -1487,7 +1487,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = | CT_lint when !optimize_fixed_int -> "((sail_int) 0xdeadc0de)", [] | CT_fbits _ -> "UINT64_C(0xdeadc0de)", [] | CT_sbits _ -> "undefined_sbits()", [] - | CT_lbits _ when !optimize_fixed_bits -> "undefined_lbits()", [] + | CT_lbits _ when !optimize_fixed_bits -> "undefined_lbits(false)", [] | CT_bool -> "false", [] | CT_enum (_, ctor :: _) -> sgen_id ctor, [] | CT_tup ctyps when is_stack_ctyp ctyp -> diff --git a/src/sail.ml b/src/sail.ml index fd13deea..2f16f130 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -192,6 +192,9 @@ let options = Arg.align ([ ( "-c_specialize", Arg.Set opt_specialize_c, " specialize integer arguments in C output"); + ( "-c_preserve", + Arg.String (fun str -> Specialize.add_initial_calls (Ast_util.IdSet.singleton (Ast_util.mk_id str))), + " make sure the provided function identifier is preserved in C output"); ( "-c_fold_unit", Arg.String (fun str -> Constant_fold.opt_fold_to_unit := Util.split_on_char ',' str), " remove comma separated list of functions from C output, replacing them with unit"); |