Changeset 776 for src/Clight/Csem.ma

Timestamp:

Apr 27, 2011, 11:47:40 AM (9 years ago)

Author:

campbell

Message:

Fix up some minor null pointer issues in Clight.
Add corresponding Cminor example and fix up pretty printer a little.

File:

• src/Clight/Csem.ma (modified) (2 diffs)

src/Clight/Csem.ma

@@ -139 +139 @@
       [ Vint n1 ⇒ match v2 with
         [ Vptr r2 b2 p2 ofs2 ⇒ Some ? (Vptr r2 b2 p2 (shift_offset ofs2 (mul (repr (sizeof ty)) n1)))
+        | Vnull r ⇒ if eq n1 zero then Some ? (Vnull r) else None ?
         | _ ⇒ None ? ]
       | _ ⇒ None ? ]
@@ -162 +163 @@
       [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
         [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ofs1 (mul (repr (sizeof ty)) n2)))
+        | _ ⇒ None ? ]
+      | Vnull r ⇒ match v2 with
+        [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ?
         | _ ⇒ None ? ]
       | _ ⇒ None ? ]