diff options
| author | Alasdair Armstrong | 2017-11-24 20:25:26 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-11-24 20:25:26 +0000 |
| commit | 381071686f99aabdc8d618051b1b63d5aeb0108c (patch) | |
| tree | eb488e0f80a76ca2699a4e5118a0c08c2ed01b69 /src/rewriter.mli | |
| parent | a1b47ed3bf5c6a4cf4d61b119c73e4fd50bea6d0 (diff) | |
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.
Diffstat (limited to 'src/rewriter.mli')
| -rw-r--r-- | src/rewriter.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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 |