diff options
| author | Jon French | 2018-09-14 15:14:18 +0100 |
|---|---|---|
| committer | Jon French | 2018-09-14 15:14:18 +0100 |
| commit | 5298ef2f1dff1e61d96842e135accab73f38824e (patch) | |
| tree | d5f8376107143bb1f439524ea2c69f4462efe431 /src/sail_lib.ml | |
| parent | b45104a529bcbe5ded4a765337b58648614481c6 (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/sail_lib.ml')
| -rw-r--r-- | src/sail_lib.ml | 9 |
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 |
