diff options
| author | Alasdair Armstrong | 2018-05-09 16:55:58 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-05-09 16:56:16 +0100 |
| commit | 0d56f6be9e2e437c570da05b1c8cdc25eb24912c (patch) | |
| tree | 4fdc1230bf8731bb4a00177d42d910713c923bca | |
| parent | c498c8a7f8d448dcefd1692e7562878cc6feb62b (diff) | |
Fix an issue with C compilation
| -rw-r--r-- | aarch64/no_vector/spec.sail | 2 | ||||
| -rw-r--r-- | lib/arith.sail | 2 | ||||
| -rw-r--r-- | src/c_backend.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/aarch64/no_vector/spec.sail b/aarch64/no_vector/spec.sail index 024393ad..775800f3 100644 --- a/aarch64/no_vector/spec.sail +++ b/aarch64/no_vector/spec.sail @@ -1374,7 +1374,7 @@ function AArch64_SysRegWrite ('op0, 'op1, 'crn, 'crm, 'op2, val_name) = assert(f val AArch64_SysRegRead : (int, int, int, int, int) -> bits(64) effect {escape, undef} -function AArch64_SysRegRead _ = { +function AArch64_SysRegRead(_, _, _, _, _) = { assert(false, "Tried to read system register"); undefined } diff --git a/lib/arith.sail b/lib/arith.sail index fa091772..54ecdbbc 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -5,7 +5,7 @@ $include <flow.sail> // ***** Addition ***** -val add_atom = {ocaml: "add_int", lem: "integerAdd"} : forall 'n 'm. +val add_atom = {ocaml: "add_int", lem: "integerAdd", c: "add_int"} : forall 'n 'm. (atom('n), atom('m)) -> atom('n + 'm) val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int"} : (int, int) -> int diff --git a/src/c_backend.ml b/src/c_backend.ml index 5cf282f9..23a8c92e 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -1927,7 +1927,7 @@ and compile_block ctx = function let setup, _, call, cleanup = compile_aexp ctx exp in let rest = compile_block ctx exps in let gs = gensym () in - setup @ [idecl CT_unit gs; call (CL_id gs)] @ cleanup @ rest + iblock (setup @ [idecl CT_unit gs; call (CL_id gs)] @ cleanup) :: rest (** Compile a sail type definition into a IR one. Most of the actual work of translating the typedefs into C is done by the code |