mark recursive predicates as [rec]

Author: cp526

src/exercises/dllist/predicates.h

@@ -1,16 +1,5 @@
 /*@
-predicate (datatype DlList) DlList_at (pointer p) {
-    if (is_null(p)) {
-        return Empty_DlList{};
-    } else {
-        take n = RW<struct dllist>(p);
-        take L = Take_Left(n.prev, p, n);
-        take R = Take_Right(n.next, p, n);
-        return Nonempty_DlList{left: L, curr: n, right: R};
-    }
-}
-
-predicate (datatype List) Take_Right (pointer p, 
+predicate [rec] (datatype List) Take_Right (pointer p, 
                                         pointer prev_pointer, 
                                         struct dllist prev_dllist) {
     if (is_null(p)) {
@@ -24,7 +13,7 @@ predicate (datatype List) Take_Right (pointer p,
     }
 }
 
-predicate (datatype List) Take_Left (pointer p, 
+predicate [rec] (datatype List) Take_Left (pointer p, 
                                          pointer next_pointer, 
                                          struct dllist next_dllist) {
     if (is_null(p)) {
@@ -37,4 +26,17 @@ predicate (datatype List) Take_Left (pointer p,
         return Cons{Head: P.data, Tail: T};
     }
 }
+
+
+predicate (datatype DlList) DlList_at (pointer p) {
+    if (is_null(p)) {
+        return Empty_DlList{};
+    } else {
+        take n = RW<struct dllist>(p);
+        take L = Take_Left(n.prev, p, n);
+        take R = Take_Right(n.next, p, n);
+        return Nonempty_DlList{left: L, curr: n, right: R};
+    }
+}
+
 @*/

src/exercises/list/cn_types.h

@@ -4,7 +4,7 @@ datatype List {
   Cons {i32 Head, datatype List Tail}
 }
 
-predicate (datatype List) SLList_At(pointer p) {
+predicate [rec] (datatype List) SLList_At(pointer p) {
   if (is_null(p)) {
     return Nil{};
   } else {

src/exercises/queue/cn_types_3.test.h

@@ -1,5 +1,5 @@
 /*@
-predicate (datatype List) QueueAux (pointer f, pointer b) {
+predicate [rec] (datatype List) QueueAux (pointer f, pointer b) {
   if (ptr_eq(f,b)) {
     return Nil{};
   } else {

src/exercises/queue/cn_types_3.verif.h

@@ -1,5 +1,5 @@
 /*@
-predicate (datatype List) QueueAux (pointer f, pointer b) {
+predicate [rec] (datatype List) QueueAux (pointer f, pointer b) {
   if (ptr_eq(f,b)) {
     return Nil{};
   } else {

src/underconstruction/bst/cn_types.h

@@ -7,7 +7,7 @@ datatype Tree {
     Node {datatype Tree Left, i32 Data, datatype Tree Right}
 } 
 
-predicate (datatype Tree) Tree_At (pointer t) 
+predicate [rec] (datatype Tree) Tree_At (pointer t) 
 {
     if (is_null(t))
     {