summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorJon French2018-09-14 15:14:18 +0100
committerJon French2018-09-14 15:14:18 +0100
commit5298ef2f1dff1e61d96842e135accab73f38824e (patch)
treed5f8376107143bb1f439524ea2c69f4462efe431 /src
parentb45104a529bcbe5ded4a765337b58648614481c6 (diff)
Sail_lib.int_of_string_opt: use Big_int.of_string rather than OCaml int_of_string
This fixes e.g. problems with 64-bit bitmask immediates in ARM assembly.
Diffstat (limited to 'src')
-rw-r--r--src/sail_lib.ml9
1 files changed, 4 insertions, 5 deletions
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index c04d469c..e7bf6348 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -508,12 +508,11 @@ let string_length str = Big_int.of_int (String.length str)
let string_append (s1, s2) = s1 ^ s2
-(* int_of_string_opt is in Ocaml stdlib but not in older versions *)
let int_of_string_opt s =
try
- Some (int_of_string s)
+ Some (Big_int.of_string s)
with
- | Failure _ -> None
+ | Invalid_argument _ -> None
(* highly inefficient recursive implementation *)
let rec maybe_int_of_prefix = function
@@ -521,13 +520,13 @@ let rec maybe_int_of_prefix = function
| str ->
let len = String.length str in
match int_of_string_opt str with
- | Some n -> ZSome (Big_int.of_int n, Big_int.of_int len)
+ | Some n -> ZSome (n, Big_int.of_int len)
| None -> maybe_int_of_prefix (String.sub str 0 (len - 1))
let maybe_int_of_string str =
match int_of_string_opt str with
| None -> ZNone ()
- | Some n -> ZSome (Big_int.of_int n)
+ | Some n -> ZSome n
let lt_int (x, y) = Big_int.less x y