Changeset 502 for Deliverables/D3.1/C-semantics/Csem.ma

Timestamp:

02/11/11 17:45:08 (2 years ago)

Author:

campbell

Message:

Fix not on nulls on Clight.

Files:

• Deliverables/D3.1/C-semantics/Csem.ma (modified) (1 diff)

Deliverables/D3.1/C-semantics/Csem.ma

@@ -96 +96 @@
       match v with
       [ Vint n ⇒ Some ? (of_bool (eq n zero))
-      | Vptr _ _ _ _ ⇒ Some ? Vfalse
       | _ ⇒ None ?
       ]
   | Tpointer _ _ ⇒
       match v with
-      [ Vint n ⇒ Some ? (of_bool (eq n zero))
-      | Vptr _ _ _ _ ⇒ Some ? Vfalse
+      [ Vptr _ _ _ _ ⇒ Some ? Vfalse
+      | Vnull _ ⇒ Some ? Vtrue
       | _ ⇒ None ?
       ]