From 8bed4e4ef414f93e02f28f0e5eb223a855ba3d14 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 17 May 2019 17:59:03 +0100
Subject: Add constraints to undefined vector functions to ensure that lengths
 are sane, and an incomplete check on undefined literals.

---
 src/initial_check.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'src/initial_check.ml')

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 522faab7..3f5592ba 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -923,9 +923,9 @@ let undefined_builtin_val_specs =
    extern_of_string (mk_id "undefined_string") "unit -> string effect {undef}";
    extern_of_string (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}";
    extern_of_string (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
-   extern_of_string (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order). (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}";
-   (* Only used with lem_mwords *)
-   extern_of_string (mk_id "undefined_bitvector") "forall 'n. atom('n) -> vector('n, dec, bit) effect {undef}";
+   extern_of_string (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order), 'n >= 0. (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}";
+   (* Only used with lem_mwords or coq *)
+   extern_of_string (mk_id "undefined_bitvector") "forall 'n, 'n >= 0. atom('n) -> vector('n, dec, bit) effect {undef}";
    extern_of_string (mk_id "undefined_unit") "unit -> unit effect {undef}"]
 
 let generate_undefineds vs_ids (Defs defs) =
-- 
cgit v1.2.3


From b87d1c27e4349cb85b9597a99c8024a59e2e0bac Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 20 May 2019 13:45:31 +0100
Subject: Revert "Add constraints to undefined vector functions to ensure that
 lengths are"

This reverts commit 8bed4e4ef414f93e02f28f0e5eb223a855ba3d14.
---
 src/initial_check.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'src/initial_check.ml')

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 3f5592ba..522faab7 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -923,9 +923,9 @@ let undefined_builtin_val_specs =
    extern_of_string (mk_id "undefined_string") "unit -> string effect {undef}";
    extern_of_string (mk_id "undefined_list") "forall ('a:Type). 'a -> list('a) effect {undef}";
    extern_of_string (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
-   extern_of_string (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order), 'n >= 0. (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}";
-   (* Only used with lem_mwords or coq *)
-   extern_of_string (mk_id "undefined_bitvector") "forall 'n, 'n >= 0. atom('n) -> vector('n, dec, bit) effect {undef}";
+   extern_of_string (mk_id "undefined_vector") "forall 'n ('a:Type) ('ord : Order). (atom('n), 'a) -> vector('n, 'ord,'a) effect {undef}";
+   (* Only used with lem_mwords *)
+   extern_of_string (mk_id "undefined_bitvector") "forall 'n. atom('n) -> vector('n, dec, bit) effect {undef}";
    extern_of_string (mk_id "undefined_unit") "unit -> unit effect {undef}"]
 
 let generate_undefineds vs_ids (Defs defs) =
-- 
cgit v1.2.3


From 239e13dc149af80f979ea95a3c9b42220481a0a1 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 4 Jun 2019 16:13:21 +0100
Subject: Remove unused AST constructor

Clean up ott grammar a bit
---
 src/initial_check.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'src/initial_check.ml')

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 522faab7..8a61134c 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -365,7 +365,6 @@ and to_ast_exp ctx (P.E_aux(exp,l) : P.exp) =
       (match to_ast_fexps false ctx exps with
       | Some(fexps) -> E_record(fexps)
       | None -> E_block(List.map (to_ast_exp ctx) exps))
-    | P.E_nondet(exps) -> E_nondet(List.map (to_ast_exp ctx) exps)
     | P.E_id(id) -> E_id(to_ast_id id)
     | P.E_ref(id) -> E_ref(to_ast_id id)
     | P.E_lit(lit) -> E_lit(to_ast_lit lit)
-- 
cgit v1.2.3