From c6710bb09c1d492b4434f0b3b375750275b4d4b5 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 4 May 2018 17:46:10 +0100
Subject: Run ARM built-in tests for Lem backend (via OCaml)

---
 lib/vector_dec.sail | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'lib')

diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 1307bb56..17603e03 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -68,11 +68,13 @@ val vector_update = {
 
 val add_bits = {
   ocaml: "add_vec",
+  lem: "add_vec",
   c: "add_bits"
 } : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 val add_bits_int = {
   ocaml: "add_vec_int",
+  lem: "add_vec_int",
   c: "add_bits_int"
 } : forall 'n. (bits('n), int) -> bits('n)
 
-- 
cgit v1.2.3


From 972d349919fc5ebe911604330ea3c80e70fdcfad Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 8 May 2018 18:48:18 +0100
Subject: Add tests for Isabelle->OCaml generation for CHERI and AArch64

---
 lib/elf.sail | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'lib')

diff --git a/lib/elf.sail b/lib/elf.sail
index e953839d..2d799d4d 100644
--- a/lib/elf.sail
+++ b/lib/elf.sail
@@ -3,11 +3,13 @@ $define _ELF
 
 val elf_entry = {
   ocaml: "Elf_loader.elf_entry",
+  lem: "elf_entry",
   c: "elf_entry"
 } : unit -> int
 
 val elf_tohost = {
   ocaml: "Elf_loader.elf_tohost",
+  lem: "elf_tohost",
   c: "elf_tohost"
 } : unit -> int
 
-- 
cgit v1.2.3


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

---
 lib/arith.sail | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

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
-- 
cgit v1.2.3