diff options
| author | Alasdair Armstrong | 2019-05-14 15:56:59 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-05-14 18:13:38 +0100 |
| commit | 94f44553d4ca93d89713b279a1d5590cb002b70f (patch) | |
| tree | fd82d65153abf686a31e2be39c99c7e9d6dc53b6 /src | |
| parent | 9d6734f717639f9babdec4441f8362bfeca10d66 (diff) | |
Various bugfixes
Since we have __deref to desugar *x in this file (as it's the one file
everything includes) we might as well add a __bitfield_deref here too,
for the bitfield setters.
Make sure undefined_nat can be used in C
Both -memo_z3 and -no_memo_z3 were listed as default options, now only
-no_memo_z3 is listed as the default.
Diffstat (limited to 'src')
| -rw-r--r-- | src/bitfield.ml | 2 | ||||
| -rw-r--r-- | src/jib/jib_smt.ml | 1 | ||||
| -rw-r--r-- | src/sail.ml | 2 |
3 files changed, 2 insertions, 3 deletions
diff --git a/src/bitfield.ml b/src/bitfield.ml index 1f64adbd..feda4602 100644 --- a/src/bitfield.ml +++ b/src/bitfield.ml @@ -121,7 +121,7 @@ let index_range_setter name field order start stop = in let irs_function = String.concat "\n" [ Printf.sprintf "function _set_%s_%s (r_ref, v) = {" name field; - " r = _reg_deref(r_ref);"; + " r = __bitfield_deref(r_ref);"; Printf.sprintf " %s;" (Util.string_of_list ";\n " body indices); " (*r_ref) = r"; "}" diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 7f622f85..5847c99c 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -1456,7 +1456,6 @@ let smt_instr ctx = | [rk; addr_size; addr; data_size] -> let mem_event, var = builtin_read_mem ctx rk addr_size addr data_size ret_ctyp in mem_event @ [define_const ctx id ret_ctyp var] - | _ -> Reporting.unreachable l __POS__ "Bad arguments for __read_mem" end diff --git a/src/sail.ml b/src/sail.ml index eff90fa3..65be5474 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -260,7 +260,7 @@ let options = Arg.align ([ "<filename>:<line>:<variable> to case split for monomorphisation"); ( "-memo_z3", Arg.Set opt_memo_z3, - " memoize calls to z3, improving performance when typechecking repeatedly (default)"); + " memoize calls to z3, improving performance when typechecking repeatedly"); ( "-no_memo_z3", Arg.Clear opt_memo_z3, " do not memoize calls to z3 (default)"); |