From 4ec8646c1bf426c848e8057cdf7c248df6999523 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 9 Nov 2022 22:03:04 +0100
Subject: Make a minor cleanup

---
 tests/betree/Primitives.fst               | 7 ++++---
 tests/betree_back_stateful/Primitives.fst | 7 ++++---
 tests/hashmap/Primitives.fst              | 7 ++++---
 tests/hashmap_on_disk/Primitives.fst      | 7 ++++---
 tests/misc/Primitives.fst                 | 7 ++++---
 5 files changed, 20 insertions(+), 15 deletions(-)

(limited to 'tests')

diff --git a/tests/betree/Primitives.fst b/tests/betree/Primitives.fst
index b44fe9d1..96138e46 100644
--- a/tests/betree/Primitives.fst
+++ b/tests/betree/Primitives.fst
@@ -47,8 +47,8 @@ let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
 (*** Scalars *)
 /// Rk.: most of the following code was at least partially generated
 
-let isize_min : int = -9223372036854775808
-let isize_max : int = 9223372036854775807
+let isize_min : int = -9223372036854775808 // TODO: should be opaque
+let isize_max : int = 9223372036854775807 // TODO: should be opaque
 let i8_min : int = -128
 let i8_max : int = 127
 let i16_min : int = -32768
@@ -60,7 +60,7 @@ let i64_max : int = 9223372036854775807
 let i128_min : int = -170141183460469231731687303715884105728
 let i128_max : int = 170141183460469231731687303715884105727
 let usize_min : int = 0
-let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max]
+let usize_max : int = 4294967295 // TODO: should be opaque
 let u8_min : int = 0
 let u8_max : int = 255
 let u16_min : int = 0
@@ -149,6 +149,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
   mk_scalar ty (x * y)
 
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
+// TODO: check the semantics of casts in Rust
 let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
   mk_scalar tgt_ty x
 
diff --git a/tests/betree_back_stateful/Primitives.fst b/tests/betree_back_stateful/Primitives.fst
index b44fe9d1..96138e46 100644
--- a/tests/betree_back_stateful/Primitives.fst
+++ b/tests/betree_back_stateful/Primitives.fst
@@ -47,8 +47,8 @@ let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
 (*** Scalars *)
 /// Rk.: most of the following code was at least partially generated
 
-let isize_min : int = -9223372036854775808
-let isize_max : int = 9223372036854775807
+let isize_min : int = -9223372036854775808 // TODO: should be opaque
+let isize_max : int = 9223372036854775807 // TODO: should be opaque
 let i8_min : int = -128
 let i8_max : int = 127
 let i16_min : int = -32768
@@ -60,7 +60,7 @@ let i64_max : int = 9223372036854775807
 let i128_min : int = -170141183460469231731687303715884105728
 let i128_max : int = 170141183460469231731687303715884105727
 let usize_min : int = 0
-let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max]
+let usize_max : int = 4294967295 // TODO: should be opaque
 let u8_min : int = 0
 let u8_max : int = 255
 let u16_min : int = 0
@@ -149,6 +149,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
   mk_scalar ty (x * y)
 
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
+// TODO: check the semantics of casts in Rust
 let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
   mk_scalar tgt_ty x
 
diff --git a/tests/hashmap/Primitives.fst b/tests/hashmap/Primitives.fst
index b44fe9d1..96138e46 100644
--- a/tests/hashmap/Primitives.fst
+++ b/tests/hashmap/Primitives.fst
@@ -47,8 +47,8 @@ let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
 (*** Scalars *)
 /// Rk.: most of the following code was at least partially generated
 
-let isize_min : int = -9223372036854775808
-let isize_max : int = 9223372036854775807
+let isize_min : int = -9223372036854775808 // TODO: should be opaque
+let isize_max : int = 9223372036854775807 // TODO: should be opaque
 let i8_min : int = -128
 let i8_max : int = 127
 let i16_min : int = -32768
@@ -60,7 +60,7 @@ let i64_max : int = 9223372036854775807
 let i128_min : int = -170141183460469231731687303715884105728
 let i128_max : int = 170141183460469231731687303715884105727
 let usize_min : int = 0
-let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max]
+let usize_max : int = 4294967295 // TODO: should be opaque
 let u8_min : int = 0
 let u8_max : int = 255
 let u16_min : int = 0
@@ -149,6 +149,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
   mk_scalar ty (x * y)
 
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
+// TODO: check the semantics of casts in Rust
 let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
   mk_scalar tgt_ty x
 
diff --git a/tests/hashmap_on_disk/Primitives.fst b/tests/hashmap_on_disk/Primitives.fst
index b44fe9d1..96138e46 100644
--- a/tests/hashmap_on_disk/Primitives.fst
+++ b/tests/hashmap_on_disk/Primitives.fst
@@ -47,8 +47,8 @@ let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
 (*** Scalars *)
 /// Rk.: most of the following code was at least partially generated
 
-let isize_min : int = -9223372036854775808
-let isize_max : int = 9223372036854775807
+let isize_min : int = -9223372036854775808 // TODO: should be opaque
+let isize_max : int = 9223372036854775807 // TODO: should be opaque
 let i8_min : int = -128
 let i8_max : int = 127
 let i16_min : int = -32768
@@ -60,7 +60,7 @@ let i64_max : int = 9223372036854775807
 let i128_min : int = -170141183460469231731687303715884105728
 let i128_max : int = 170141183460469231731687303715884105727
 let usize_min : int = 0
-let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max]
+let usize_max : int = 4294967295 // TODO: should be opaque
 let u8_min : int = 0
 let u8_max : int = 255
 let u16_min : int = 0
@@ -149,6 +149,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
   mk_scalar ty (x * y)
 
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
+// TODO: check the semantics of casts in Rust
 let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
   mk_scalar tgt_ty x
 
diff --git a/tests/misc/Primitives.fst b/tests/misc/Primitives.fst
index b44fe9d1..96138e46 100644
--- a/tests/misc/Primitives.fst
+++ b/tests/misc/Primitives.fst
@@ -47,8 +47,8 @@ let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
 (*** Scalars *)
 /// Rk.: most of the following code was at least partially generated
 
-let isize_min : int = -9223372036854775808
-let isize_max : int = 9223372036854775807
+let isize_min : int = -9223372036854775808 // TODO: should be opaque
+let isize_max : int = 9223372036854775807 // TODO: should be opaque
 let i8_min : int = -128
 let i8_max : int = 127
 let i16_min : int = -32768
@@ -60,7 +60,7 @@ let i64_max : int = 9223372036854775807
 let i128_min : int = -170141183460469231731687303715884105728
 let i128_max : int = 170141183460469231731687303715884105727
 let usize_min : int = 0
-let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max]
+let usize_max : int = 4294967295 // TODO: should be opaque
 let u8_min : int = 0
 let u8_max : int = 255
 let u16_min : int = 0
@@ -149,6 +149,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
   mk_scalar ty (x * y)
 
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
+// TODO: check the semantics of casts in Rust
 let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
   mk_scalar tgt_ty x
 
-- 
cgit v1.2.3