Split Class into ByReferenceClass and ByValueClass

build.sc

@@ -41,7 +41,7 @@ object external extends Module {
 object viper extends ScalaModule {
   object silverGit extends GitModule {
     def url = T { "https://github.com/viperproject/silver.git" }
-    def commitish = T { "4a8065758868eae3414f86f3d96e843a283444fc" }
+    def commitish = T { "93bc9b7516a710c8f01438e430058c4a54e20512" }
     def filteredRepo = T {
       val workspace = repo()
       os.remove.all(workspace / "src" / "test")
@@ -50,8 +50,8 @@ object viper extends ScalaModule {
   }
 
   object siliconGit extends GitModule {
-    def url = T { "https://github.com/viperproject/silicon.git" }
-    def commitish = T { "4033dd21614b3bbba9c7615655e41c6cf0b9d80b" }
+    def url = T { "https://github.com/superaxander/silicon.git" }
+    def commitish = T { "c63989f64eb759f33bde68c330ce07d6e34134fa" }
     def filteredRepo = T {
       val workspace = repo()
       os.remove.all(workspace / "src" / "test")

examples/concepts/c/pointer_casts.c

@@ -0,0 +1,90 @@
+#include <stdbool.h>
+
+struct A {
+    int integer;
+    bool boolean;
+};
+
+struct B {
+    struct A struct_a;
+};
+
+void canCastToInteger() {
+    struct B struct_b;
+    struct_b.struct_a.integer = 5;
+    int *pointer_to_integer = (int *)&struct_b;
+    //@ assert *pointer_to_integer == 5;
+    //@ assert pointer_to_integer == &struct_b.struct_a.integer;
+    //@ assert pointer_to_integer == (int *)&struct_b.struct_a;
+    // The following is not implemented yet
+    // assert pointer_to_integer == &struct_b
+    // assert pointer_to_integer == &struct_b.struct_a
+    *pointer_to_integer = 10;
+    //@ assert struct_b.struct_a.integer == 10;
+}
+
+
+void castRemainsValidInLoop() {
+    struct B struct_b;
+    struct_b.struct_a.integer = 10;
+
+    int *pointer_to_integer = (int *)&struct_b;
+
+    //@ loop_invariant 0 <= i && i <= 10;
+    //@ loop_invariant Perm(&struct_b, write);
+    //@ loop_invariant Perm(struct_b, write);
+    //@ loop_invariant pointer_to_integer == (int *)&struct_b;
+    //@ loop_invariant *pointer_to_integer == 10 - i;
+    for (int i = 0; i < 10; i++) {
+        *pointer_to_integer = *pointer_to_integer - 1;
+    }
+
+    //@ assert struct_b.struct_a.integer == 0;
+    struct_b.struct_a.integer = 10;
+
+    // We can also specify the permission through the pointer
+    //@ loop_invariant 0 <= i && i <= 10;
+    //@ loop_invariant Perm(pointer_to_integer, write);
+    //@ loop_invariant *pointer_to_integer == 10 - i;
+    for (int i = 0; i < 10; i++) {
+        *pointer_to_integer = *pointer_to_integer - 1;
+    }
+
+    //@ assert struct_b.struct_a.integer == 0;
+}
+
+void castRemainsValidInParBlock() {
+    struct B struct_b;
+    struct_b.struct_a.integer = 10;
+
+    int *pointer_to_integer = (int *)&struct_b;
+
+    //@ context i == 8 ==> Perm(pointer_to_integer, write);
+    //@ ensures i == 8 ==> *pointer_to_integer == 0;
+    for (int i = 0; i < 10; i++) {
+        if (i == 8) {
+            *pointer_to_integer = *pointer_to_integer - 10;
+        }
+    }
+
+    // Unfortunately we don't support a par block where we specify permission to the struct and then access through the cast (the generated cast helper is put too far away)
+
+    //@ assert struct_b.struct_a.integer == 0;
+}
+
+//@ requires a != NULL;
+//@ context Perm(a, write);
+//@ ensures *a == \old(*a) + 1;
+void increaseByOne(int *a) {
+    *a += 1;
+}
+
+void callWithCast() {
+    struct B struct_b;
+    struct_b.struct_a.integer = 15;
+
+    int *pointer_to_integer = (int *)&struct_b;
+    increaseByOne(pointer_to_integer);
+
+    //@ assert struct_b.struct_a.integer == 16;
+}

examples/concepts/c/structs.c

@@ -21,8 +21,8 @@ struct linked_list{
 
 /*@
     context p != NULL ** Perm(p, write);
-    context Perm(p->x, write);
-    context Perm(p->y, write);
+    context Perm(&p->x, write);
+    context Perm(&p->y, write);
     ensures p->x == 0;
     ensures p->y == 0;
     ensures \old(*p) == *p;
@@ -44,14 +44,15 @@ void alter_struct_1(struct point *p){
 }
 
 /*@
-  context Perm(p.x, 1\1);
-  context Perm(p.y, 1\1);
+  context Perm(&p.x, 1\1);
+  context Perm(&p.y, 1\1);
 @*/
 void alter_copy_struct(struct point p){
     p.x = 0;
     p.y = 0;
 }
 
+// TODO: Should be auto-generated
 /*@
   context Perm(p, 1\1);
 @*/
@@ -75,7 +76,7 @@ int avr_x(struct triangle *r){
  requires inp != NULL && \pointer_length(inp) >= n;
  requires (\forall* int i; 0 <= i && i < n; Perm(&inp[i], 1\10));
  requires (\forall int i, int j; 0<=i && i<n && 0<=j && j<n; i != j ==> {:inp[i]:} != {:inp[j]:});
- requires (\forall* int i; 0 <= i && i < n; Perm(inp[i].x, 1\10));
+ requires (\forall* int i; 0 <= i && i < n; Perm(&inp[i].x, 1\10));
  ensures |\result| == n;
  ensures (\forall int i; 0 <= i && i < n; \result[i] == inp[i].x);
  //ensures n>0 ==> \result == inp_to_seq(inp, n-1) + [inp[n-1].x];
@@ -132,7 +133,7 @@ int main(){
     struct point *pp;
     pp = &p;
 
-    //@ assert (pp[0] != NULL );
+    /* //@ assert (pp[0] != NULL ); */
     assert (pp != NULL );
 
     p.x = 1;
@@ -168,4 +169,4 @@ int main(){
     assert(avr_pol == 2);
 
     return 0;
-}
+}

res/universal/res/adt/pointer.pvl

@@ -16,6 +16,7 @@ adt `pointer` {
   pure `pointer` pointer_of(`block` b, int offset);
   pure `block` pointer_block(`pointer` p);
   pure int pointer_offset(`pointer` p);
+  pure `pointer` pointer_inv(ref r);
 
   // the block offset is valid wrt the length of the block
   axiom (∀ `pointer` p;
@@ -26,6 +27,10 @@ adt `pointer` {
   axiom (∀`block` b, int offset;
     {:pointer_block(pointer_of(b, offset)):} == b &&
       {:pointer_offset(pointer_of(b, offset)):} == offset);
+
+  axiom (∀ ref r; ptr_deref({:pointer_inv(r):}) == r);
+
+  axiom (∀ `pointer` p; pointer_inv({:ptr_deref(p):}) == p);
 }
 
 decreases;
@@ -38,4 +43,4 @@ requires `pointer`.pointer_offset(p) + offset < `block`.block_length(`pointer`.p
 pure `pointer` ptr_add(`pointer` p, int offset) =
   `pointer`.pointer_of(
      `pointer`.pointer_block(p),
-     `pointer`.pointer_offset(p) + offset);
+     `pointer`.pointer_offset(p) + offset);