From 381071686f99aabdc8d618051b1b63d5aeb0108c Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 24 Nov 2017 20:25:26 +0000
Subject: Use unbound precision big_ints throughout sail.

Alastair's test cases revealed that using regular ints causes issues
throughout sail, where all kinds of things can internally overflow in
edge cases. This either causes crashes (e.g. int_of_string fails for
big ints) or bizarre inexplicable behaviour. This patch switches the
sail AST to use big_int rather than int, and updates everything
accordingly.

This touches everything and there may be bugs where I mistranslated
things, and also n = m will still typecheck with big_ints but fail at
runtime (ocaml seems to have decided that static typing is unnecessary
for equality...), as it needs to be changed to eq_big_int.

I also got rid of the old unused ocaml backend while I was updating
things, so as to not have to fix it.
---
 src/rewriter.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/rewriter.mli')

diff --git a/src/rewriter.mli b/src/rewriter.mli
index 412852d4..c107be25 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -53,7 +53,7 @@ type 'a rewriters = { rewrite_exp  : 'a rewriters -> 'a exp -> 'a exp;
                       rewrite_def  : 'a rewriters -> 'a def -> 'a def;
                       rewrite_defs : 'a rewriters -> 'a defs -> 'a defs;
                     }
-                    
+
 val rewrite_exp : tannot rewriters -> tannot exp -> tannot exp
 val rewrite_defs : tannot defs -> tannot defs
 val rewrite_undefined : bool -> tannot defs -> tannot defs
-- 
cgit v1.2.3