Merge pull request #45 from rems-project/owned-disjoint-update

Update tutorial and examples for Owned disjoint

src/examples/list_c_types.h

@@ -7,8 +7,7 @@ extern struct int_list *mallocIntList();
 /*@ spec mallocIntList();
     requires true;
     ensures take u = Block<struct int_list>(return);
-            !ptr_eq(return, NULL);
-@*/ // 'return != NULL' should not be needed
+@*/
 
 extern void freeIntList (struct int_list *p);
 /*@ spec freeIntList(pointer p);

src/examples/queue_allocation.h

@@ -2,7 +2,6 @@ extern struct int_queue *mallocIntQueue();
 /*@ spec mallocIntQueue();
     requires true;
     ensures take u = Block<struct int_queue>(return);
-            !ptr_eq(return,NULL);
 @*/ 
 
 extern void freeIntQueue (struct int_queue *p);
@@ -15,7 +14,6 @@ extern struct int_queueCell *mallocIntQueueCell();
 /*@ spec mallocIntQueueCell();
     requires true;
     ensures take u = Block<struct int_queueCell>(return);
-            !is_null(return);
 @*/ 
 
 extern void freeIntQueueCell (struct int_queueCell *p);

src/examples/queue_push_induction.c

@@ -1,33 +1,27 @@
 #include "queue_headers.h" 
 
-/*@
-lemma assert_not_equal(pointer x, pointer y)
-requires
-    true;
-ensures
-    !ptr_eq(x, y);
-@*/
-
-void push_induction(struct int_queueCell* front, struct int_queueCell* p)
+void push_induction(struct int_queueCell* front
+        , struct int_queueCell* second_last
+        , struct int_queueCell* last)
 /*@
   requires
-      take Q = IntQueueAux(front, p);
-      take P = Owned(p);
-      !ptr_eq(front, P.next);
-      !is_null(P.next);
+      take Q = IntQueueAux(front, second_last);
+      take Second_last = Owned(second_last);
+      ptr_eq(Second_last.next, last);
+      take Last = Owned(last);
   ensures
-      take NewQ = IntQueueAux(front, P.next);
-      NewQ == snoc(Q, P.first);
+      take NewQ = IntQueueAux(front, last);
+      take Last2 = Owned(last);
+      NewQ == snoc(Q, Second_last.first);
+      Last == Last2;
 @*/
 {
-    if (front == p) {
-        /*@ unfold snoc(Q, P.first); @*/
+    if (front == second_last) {
+        /*@ unfold snoc(Q, Second_last.first); @*/
         return;
     } else {
-        // Should be derived automatically
-        /*@ apply assert_not_equal((*front).next, (*p).next); @*/
-        push_induction(front->next, p);
-        /*@ unfold snoc(Q, P.first); @*/
+        push_induction(front->next, second_last, last);
+        /*@ unfold snoc(Q, Second_last.first); @*/
         return;
     }
 }
@@ -39,7 +33,6 @@ void IntQueue_push (int x, struct int_queue *q)
 @*/
 {
   struct int_queueCell *c = mallocIntQueueCell();
-  /*@ apply assert_not_equal((*q).front, c); @*/
   c->first = x;
   c->next = 0;
   if (q->back == 0) {
@@ -50,7 +43,7 @@ void IntQueue_push (int x, struct int_queue *q)
     struct int_queueCell *oldback = q->back;
     q->back->next = c;
     q->back = c;
-    push_induction(q->front, oldback);
+    push_induction(q->front, oldback, c);
     return;
   }
 }

src/tutorial.adoc

@@ -715,15 +715,6 @@ in the pre- and postconditions that captures both cases together:
 
 include_example(exercises/slf_incr2.c)
 
-**Note**: At the moment, CN does not derive pointer disjointness
-constraints from resources: from simultaneous ownership of the
-resources `+Owned(p)+` and `+Owned(q)+` CN does not automatically
-learn `+(p != q)+`, even though that’s clearly implied. This was
-turned off for performance reasons at some point, but once
-performance is back to normal again it should come back.  In the mean
-time, we have to add `+(p != q)+` as an additional precondition to
-`+call_both+`.
-
 == Allocating and Deallocating Memory
 
 At the moment, CN does not understand the `+malloc+` and `+free+`