Merge branch 'sail2' of github.com:rems-project/sail into sail2

3 files changed, 22 insertions, 2 deletions

diff --git a/lib/elf.sail b/lib/elf.sail
index f158fbad..e953839d 100644
--- a/lib/elf.sail
+++ b/lib/elf.sail
@@ -1,8 +1,14 @@
 $ifndef _ELF
 $define _ELF
 
-val elf_entry = "Elf_loader.elf_entry" : unit -> int
+val elf_entry = {
+  ocaml: "Elf_loader.elf_entry",
+  c: "elf_entry"
+} : unit -> int
 
-val elf_tohost = "Elf_loader.elf_tohost" : unit -> int
+val elf_tohost = {
+  ocaml: "Elf_loader.elf_tohost",
+  c: "elf_tohost"
+} : unit -> int
 
 $endif
diff --git a/lib/flow.sail b/lib/flow.sail
index 8c902803..1a0e0f2f 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -34,6 +34,8 @@ val lt_int = "lt" : (int, int) -> bool
 val gt_int = "lt" : (int, int) -> bool
 
 overload operator == = {eq_atom, eq_range, eq_int}
+overload operator | = {or_bool}
+overload operator & = {and_bool}
 
 $ifdef TEST
 
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index e24f5111..8a55ed61 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -13,6 +13,18 @@ val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
 /* Used for creating long bitvector literals in the C backend. */
 val "append_64" : forall 'n. (bits('n), bits(64)) -> bits('n + 64)
 
+val vector_access = {
+  ocaml: "access",
+  lem: "access_list_dec",
+  c: "vector_access"
+} : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m)) -> 'a
+
+val vector_update = {
+  ocaml: "update",
+  lem: "update_list_dec",
+  c: "vector_update"
+} : forall 'n ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
+
 val add_bits = {
   ocaml: "add_vec",
   c: "add_bits"