Changeset 1920 for src/Clight/Csyntax.ma

Timestamp:

May 8, 2012, 11:16:18 AM (8 years ago)

Author:

campbell

Message:

Most of the labelling simulation. Still need to sort out switch statements
and function calls.

File:

• src/Clight/Csyntax.ma (modified) (1 diff)

src/Clight/Csyntax.ma

@@ -208 +208 @@
   | LSdefault: statement → labeled_statements
   | LScase: ∀sz:intsize. bvint sz → statement → labeled_statements → labeled_statements.
+
+let rec labeled_statements_ind
+  (P:labeled_statements → Prop)
+  (LSd:∀s. P (LSdefault s))
+  (LSc:∀sz,i,s,tl. P tl → P (LScase sz i s tl))
+  ls on ls : P ls ≝
+match ls with
+[ LSdefault s ⇒ LSd s
+| LScase sz i s tl ⇒ LSc sz i s tl (labeled_statements_ind P LSd LSc tl)
+].
 
 let rec statement_ind2