summaryrefslogtreecommitdiff
path: root/src/spec_analysis.mli
diff options
context:
space:
mode:
authorKathy Gray2016-01-21 11:41:51 +0000
committerKathy Gray2016-01-21 11:42:04 +0000
commitb14c153524a0cc7e8981d96ea85f7abfd255249a (patch)
tree6914331949bc327ebd47fe0ae541aea02164fe9f /src/spec_analysis.mli
parent6728534f7561c93a97063e3ac4f6e3c1bc7cfdee (diff)
Start splitting values/etc into int/big_int for ocaml generation
Diffstat (limited to 'src/spec_analysis.mli')
-rw-r--r--src/spec_analysis.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli
index 1b1197dd..731bd822 100644
--- a/src/spec_analysis.mli
+++ b/src/spec_analysis.mli
@@ -17,3 +17,4 @@ val default_order : tannot defs -> order
suitable unwrapping of abbreviations, reg, and registers).
*)
val is_within_range: typ -> typ -> nexp_range list -> triple
+val is_within_machine64 : typ -> nexp_range list -> triple