Permalink
Browse files

Add ptr1_is_null and ptr1_isnot_null

  • Loading branch information...
1 parent bc22513 commit 78683476144d200e1868462155fdc6926768b892 @doublec committed Apr 30, 2012
Showing with 67 additions and 1 deletion.
  1. +48 −0 ats-reference.txt
  2. +11 −1 pointer/Makefile
  3. +4 −0 pointer/ptr1_is_null.dats
  4. +4 −0 pointer/ptr1_isnot_null.dats
View
@@ -1073,3 +1073,51 @@ implement main() = {
val () = print (a)
}
----
+
+ptr1_is_null
+~~~~~~~~~~~~
+
+Definition
+^^^^^^^^^^
+----
+fun ptr1_is_null {l:addr}
+ (p: ptr l):<> bool (l==null)
+----
+
+Description
+^^^^^^^^^^^
+Given a dependently typed pointer indexed by the address value, return 'true' if the pointer is NULL.
+
+Example
+^^^^^^^
+----
+implement main() = {
+ val a = null
+ val () = assertloc (ptr1_is_null (a))
+}
+----
+
+ptr1_isnot_null
+~~~~~~~~~~~~~~~
+
+Definition
+^^^^^^^^^^
+----
+fun ptr1_isnot_null {l:addr}
+ (p: ptr l):<> bool (l > null)
+overload ~ with ptr1_isnot_null
+----
+
+Description
+^^^^^^^^^^^
+Given a dependently typed pointer indexed by the address value, return 'true'
+if the pointer is not NULL.
+
+Example
+^^^^^^^
+----
+implement main() = {
+ val a = null + 4
+ val () = assertloc (ptr1_isnot_null (a))
+}
+----
View
@@ -3,7 +3,9 @@ all: ptr_is_null \
add_ptr \
sub_ptr \
ptr1_of_ptr \
- null
+ null \
+ ptr1_is_null \
+ ptr1_isnot_null
ptr_is_null: ptr_is_null.dats
atscc -o ptr_is_null ptr_is_null.dats
@@ -23,6 +25,12 @@ ptr1_of_ptr: ptr1_of_ptr.dats
null: null.dats
atscc -o null null.dats
+ptr1_is_null: ptr1_is_null.dats
+ atscc -o ptr1_is_null ptr1_is_null.dats
+
+ptr1_isnot_null: ptr1_isnot_null.dats
+ atscc -o ptr1_isnot_null ptr1_isnot_null.dats
+
clean:
-rm *_dats.c
@@ -33,5 +41,7 @@ clean:
-rm sub_ptr
-rm ptr1_of_ptr
-rm null
+ -rm ptr1_is_null
+ -rm ptr1_isnot_null
@@ -0,0 +1,4 @@
+implement main() = {
+ val a = null
+ val () = assertloc (ptr1_is_null (a))
+}
@@ -0,0 +1,4 @@
+implement main() = {
+ val a = null + 4
+ val () = assertloc (ptr1_isnot_null (a))
+}

0 comments on commit 7868347

Please sign in to comment.