summaryrefslogtreecommitdiff
path: root/src/lem_interp
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp')
-rw-r--r--src/lem_interp/interp.lem2
-rw-r--r--src/lem_interp/interp_interface.lem4
-rw-r--r--src/lem_interp/interp_lib.lem6
3 files changed, 6 insertions, 6 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index addc37ba..bf2feedf 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -1688,7 +1688,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
(fun tlv lm le -> match detaint tlv with
| V_list t -> (Value (retaint tlv (V_list (hdv::t))),lm,le)
| V_unknown -> (Value (retaint tlv V_unknown),lm,le)
- | _ -> (Error l "Internal error '::' of non-list value",lm,le) end)
+ | _ -> (Error l ("Internal error '::' of non-list value " ^ (string_of_value tlv)),lm,le) end)
(fun a -> update_stack a
(add_to_top_frame
(fun t env -> let (hde,env') = to_exp mode env hdv in (E_aux (E_cons hde t) (l,annot),env')))))
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 5473e1a0..2850332e 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -201,8 +201,8 @@ instance (Ord byte)
let (>=) = byteGreaterEq
end
-let ~{ocaml} addressCompare (Address b1 i1) (Address b2 i2) = compare i1 i2
-let inline {ocaml} addressCompare = defaultCompare
+let (*~{ocaml}*) addressCompare (Address b1 i1) (Address b2 i2) = compare i1 i2
+(*let inline {ocaml} addressCompare = defaultCompare*)
let ~{ocaml} addressLess b1 b2 = addressCompare b1 b2 = LT
let ~{ocaml} addressLessEq b1 b2 = addressCompare b1 b2 <> GT
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 1c70a97b..141dd6f4 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -30,9 +30,9 @@ let hardware_quot (a:integer) (b:integer) : integer =
let (max_64u : integer) = integerFromNat ((natPow 2 64) - 1)
let (max_64 : integer) = integerFromNat ((natPow 2 63) - 1)
let (min_64 : integer) = integerNegate (integerFromNat (natPow 2 63))
-let (max_32u : integer) = integerFromNat 4294967295
-let (max_32 : integer) = integerFromNat 2147483647
-let (min_32 : integer) = integerNegate (integerFromNat 2147483648)
+let (max_32u : integer) = integerFromNat (natPow 2 32) (*4294967295*)
+let (max_32 : integer) = integerFromNat ((natPow 2 31) - 1) (*2147483647*)
+let (min_32 : integer) = integerNegate (integerFromNat (natPow 2 31)) (*2147483648*)
let (max_8 : integer) = (integerFromNat 127)
let (min_8 : integer) = (integerFromNat 0) - (integerFromNat 128)
let (max_5 : integer) = (integerFromNat 31)