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)

---
 test/builtins/test_extras.lem | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 test/builtins/test_extras.lem

(limited to 'test/builtins/test_extras.lem')

diff --git a/test/builtins/test_extras.lem b/test/builtins/test_extras.lem
new file mode 100644
index 00000000..136f680e
--- /dev/null
+++ b/test/builtins/test_extras.lem
@@ -0,0 +1,22 @@
+open import Pervasives_extra
+open import Sail_instr_kinds
+open import Sail_values
+open import Sail_operators_mwords
+open import Prompt_monad
+open import State
+
+type ty0
+instance (Size ty0) let size = 0 end
+declare isabelle target_rep type ty1 = `0`
+
+val undefined_int : forall 'rv 'e. unit -> monad 'rv integer 'e
+let undefined_int () = return 0
+
+val undefined_bitvector : forall 'rv 'a 'e. Size 'a => integer -> monad 'rv (mword 'a) 'e
+let undefined_bitvector len = return (zeros(len))
+
+val undefined_unit : forall 'rv 'e. unit -> monad 'rv unit 'e
+let undefined_unit () = return ()
+
+val internal_pick : forall 'rv 'a 'e. list 'a -> monad 'rv 'a 'e
+let internal_pick xs = return (List_extra.head xs)
-- 
cgit v1.2.3