diff options
| author | Jon French | 2019-02-25 12:10:30 +0000 |
|---|---|---|
| committer | Jon French | 2019-02-25 12:10:30 +0000 |
| commit | 915d75f9c49fa2c2a9d47d189e4224cee16582c9 (patch) | |
| tree | 77a93e682796977898af0b56e0a61d7689db112e /language/bytecode.ott | |
| parent | a8a5308e4981b3d09fb2bf0c59d592ef6ae4417e (diff) | |
| parent | 38656b50ad24df6a29f3a84e50adfcf409131fb0 (diff) | |
Merge branch 'sail2' into rmem_interpreter
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 |