diff options
| author | Alasdair Armstrong | 2018-06-21 16:22:03 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-06-21 17:02:01 +0100 |
| commit | bb694008780f63d84a68893016044b660a1558bf (patch) | |
| tree | 9cef428d8f19673459a07f8387df4b423bba5505 /language/bytecode.ott | |
| parent | 326f0dd88df92d3936b7acadb5073802d3f9d77b (diff) | |
| parent | 3658789d204eb100e901a2adb67b6bf8a30157bf (diff) | |
Merge branch 'tracing' into sail2
Diffstat (limited to 'language/bytecode.ott')
| -rw-r--r-- | language/bytecode.ott | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/language/bytecode.ott b/language/bytecode.ott index 704bda83..895ac34b 100644 --- a/language/bytecode.ott +++ b/language/bytecode.ott @@ -65,11 +65,11 @@ fragment :: 'F_' ::= ctyp :: 'CT_' ::= {{ com C type }} - | mpz_t :: :: mpz + | mpz_t :: :: int % Arbitrary precision GMP integer, mpz_t in C. }} - | bv_t ( bool ) :: :: bv + | bv_t ( bool ) :: :: bits % Variable length bitvector - flag represents direction, true - dec or false - inc }} - | 'uint64_t' ( nat , bool ) :: :: uint64 + | 'uint64_t' ( nat , bool ) :: :: bits64 % Fixed length bitvector that fits within a 64-bit word. - int % represents length, and flag is the same as CT_bv. }} | 'int64_t' :: :: int64 @@ -122,7 +122,6 @@ iannot :: 'IA_' ::= instr :: 'I_' ::= {{ aux _ iannot }} | ctyp id :: :: decl - | alloc ctyp id :: :: alloc | ctyp id = cval :: :: init | if ( cval ) { instr0 ; ... ; instrn } else { instr0 ; ... ; instrm } : ctyp :: :: if @@ -150,8 +149,6 @@ cdef :: 'CDEF_' ::= | ctype_def :: :: type | let nat ( id0 : ctyp0 , ... , idn : ctypn ) = { instr0 ; ... ; instrm - } { - instr0 ; ... ; instri } :: :: let % The first list of instructions creates up the global letbinding, the % second kills it. |