Changeset 816 for src/RTLabs/syntax.ma

Timestamp:

May 19, 2011, 3:06:42 PM (10 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:

• src/RTLabs/syntax.ma (modified) (1 diff)

src/RTLabs/syntax.ma

@@ -45 +45 @@
 | St_load : memory_chunk → ∀m:addressing. addr m → register → label → statement
 | St_store : memory_chunk → ∀m:addressing. addr m → register → label → statement
-| St_call_id : ident → list register → option register → signature → label → statement
-| St_call_ptr : register → list register → option register → signature → label → statement
-| St_tailcall_id : ident → list register → signature → statement
-| St_tailcall_ptr : register → list register → signature → statement
+| St_call_id : ident → list register → option register → label → statement
+| St_call_ptr : register → list register → option register → label → statement
+| St_tailcall_id : ident → list register → statement
+| St_tailcall_ptr : register → list register → statement
 (* Um, what? *)
 | St_condcst : constant → label → label → statement