diff options
| author | Alasdair | 2019-02-22 20:50:16 +0000 |
|---|---|---|
| committer | Alasdair | 2019-02-22 20:55:41 +0000 |
| commit | 38656b50ad24df6a29f3a84e50adfcf409131fb0 (patch) | |
| tree | 9e49f5197125d721dbe6b22ecfb8c4ace2755961 /language/bytecode.ott | |
| parent | fc9e071bb633fd7c7241db79146934e4ab2b33b5 (diff) | |
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.
Diffstat (limited to 'language/bytecode.ott')
| -rw-r--r-- | language/bytecode.ott | 4 |
1 files changed, 2 insertions, 2 deletions
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 |