Changeset 225 for C-semantics

Timestamp:

Nov 9, 2010, 12:52:32 PM (10 years ago)

Author:

campbell

Message:

Missing case in cast.

File:

• C-semantics/CexecIO.ma (modified) (2 diffs)

C-semantics/CexecIO.ma

@@ -164 +164 @@
 [ true ⇒
   match ty with
-  [ Tpointer _ _ ⇒
+  [ Tint _ _ ⇒
+    match ty' with
+    [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
+    | Tarray _ _ _ ⇒ Some ? (OK ? (Vint i))
+    | Tfunction _ _ ⇒ Some ? (OK ? (Vint i))
+    | _ ⇒ Some ? (Error ?)
+    ]
+  | Tpointer _ _ ⇒
     match ty' with
     [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
@@ -189 +196 @@
 | false ⇒ Some ? (Error ?)
 ]. nwhd; //; nlapply (eq_spec i zero); nrewrite > c0; #e; nrewrite > e;
-   napply cast_pp_z; //; nqed. 
+   ##[ ##1,2,3: napply cast_ip_z ##| ##*: napply cast_pp_z ##] //; nqed. 
 
 ndefinition ms_eq_dec : ∀s1,s2:memory_space. (s1 = s2) + (s1 ≠ s2).