Changeset 816 for src/RTLabs/syntax.ma


Ignore:
Timestamp:
May 19, 2011, 3:06:42 PM (9 years ago)
Author:
campbell
Message:

Clight to Cminor compilation, modulo switch statements, temporary
generation, 32 to 8 bit translation and miscellaneous bugs.

Also, remove (unused) signatures from function call statements in Cminor
and RTLabs; and separate comparison of integers and pointers in Clight
semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/syntax.ma

    r765 r816  
    4545| St_load : memory_chunk → ∀m:addressing. addr m → register → label → statement
    4646| St_store : memory_chunk → ∀m:addressing. addr m → register → label → statement
    47 | St_call_id : ident → list register → option register → signature → label → statement
    48 | St_call_ptr : register → list register → option register → signature → label → statement
    49 | St_tailcall_id : ident → list register → signature → statement
    50 | St_tailcall_ptr : register → list register → signature → statement
     47| St_call_id : ident → list register → option register → label → statement
     48| St_call_ptr : register → list register → option register → label → statement
     49| St_tailcall_id : ident → list register → statement
     50| St_tailcall_ptr : register → list register → statement
    5151(* Um, what? *)
    5252| St_condcst : constant → label → label → statement
Note: See TracChangeset for help on using the changeset viewer.