From 38656b50ad24df6a29f3a84e50adfcf409131fb0 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Fri, 22 Feb 2019 20:50:16 +0000
Subject: Generalize CT_int64 for arbitrary fixed size integers

If we want to use our low-level intermediate representation to generate
SMT, then we want to be more precise than just splitting integers into
64-bits and larger. This commit changes CT_int and CT_int64 into CT_lint
for large integers and CT_fint n for (signed) fixed precision integers
that fit within n bits. This follows the convention for bitvectors where
we have CT_fbits for fixed-length bitvectors and CT_lbits for large
arbitrary precision bitvectors.
---
 language/bytecode.ott | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'language/bytecode.ott')

diff --git a/language/bytecode.ott b/language/bytecode.ott
index d2580e8c..cc329e02 100644
--- a/language/bytecode.ott
+++ b/language/bytecode.ott
@@ -66,7 +66,7 @@ fragment :: 'F_' ::=
 
 ctyp :: 'CT_' ::=
   {{ com C type }}
-  | mpz_t                     :: :: int
+  | mpz_t                     :: :: lint
 % Arbitrary precision GMP integer, mpz_t in C.
   | bv_t ( bool )             :: :: lbits
 % Variable length bitvector - flag represents direction, true - dec or false - inc
@@ -75,7 +75,7 @@ ctyp :: 'CT_' ::=
   | 'uint64_t' ( nat , bool ) :: :: fbits
 % Fixed length bitvector that fits within a 64-bit word. - int
 % represents length, and flag is the same as CT_bv.
-  | 'int64_t'                 :: :: int64
+  | 'int64_t' nat             :: :: fint
 % Used for (signed) integers that fit within 64-bits.
   | unit_t                    :: :: unit
 % unit is a value in sail, so we represent it as a one element type
-- 
cgit v1.2.3