From 0d56f6be9e2e437c570da05b1c8cdc25eb24912c Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 9 May 2018 16:55:58 +0100
Subject: Fix an issue with C compilation

---
 aarch64/no_vector/spec.sail | 2 +-
 lib/arith.sail              | 2 +-
 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
-- 
cgit v1.2.3