Merge remote-tracking branch 'origin/dev' into small-fix

examples/concepts/generics/box.pvl

@@ -0,0 +1,14 @@
+class Box<T> {
+  T t;
+  context Perm(t, 1\2);
+  ensures \result == t;
+  T get() {
+    return t;
+  }
+}
+
+void m() {
+  Box<int> b = new Box<int>();
+  int t = b.get();
+  int t = b.t;
+}

examples/concepts/generics/genericChannel.pvl

@@ -0,0 +1,65 @@
+lock_invariant Perm(transfering, 1) ** Perm(exchangeValue,1);
+class Chan<T> {
+  boolean transfering;
+  T exchangeValue;
+
+  ensures committed(this);
+  constructor() {
+    transfering = false;
+    commit this;
+  }
+
+  context committed(this);
+  void writeValue(T v) {
+    lock this;
+
+    loop_invariant Perm(transfering, 1) ** Perm(exchangeValue,1);
+    loop_invariant held(this);
+    while (!transfering) {
+      unlock this;
+      lock this;
+    }
+
+    transfering = false;
+    exchangeValue = v;
+    unlock this;
+  }
+
+  context committed(this);
+  T readValue() {
+    lock this;
+
+    loop_invariant Perm(transfering, 1) ** Perm(exchangeValue,1);
+    loop_invariant held(this);
+    while (transfering) {
+      unlock this;
+      lock this;
+    }
+
+    T m = exchangeValue;
+    transfering = false;
+    unlock this;
+
+    return m;
+  }
+
+  context committed(this);
+  T noop(T t) {
+    writeValue(t);
+    return readValue();
+  }
+}
+
+void main() {
+  Chan<int> intChan = new Chan<int>();
+  Chan<boolean> boolChan = new Chan<boolean>();
+  Chan<Chan<int>> intChanChan = new Chan<Chan<int>>();
+
+  intChan.writeValue(5);
+  boolChan.writeValue(true);
+  intChanChan.writeValue(intChan);
+
+  int i = intChan.readValue();
+  boolean b = boolChan.readValue();
+  Chan<int> c = intChanChan.readValue();
+}

examples/concepts/generics/genericProcedure.pvl

@@ -0,0 +1,4 @@
+ensures \result == t;
+T myProcedure<T>(T t) {
+  return t;
+}

examples/technical/java/generics/MyRetention.java

@@ -0,0 +1,13 @@
+import java.lang.annotation.Retention;
+
+class C {
+    Retention r;
+}
+
+class D<T> { }
+
+class E {
+    void m() {
+        D<?> d = null;
+    }
+}

examples/technical/veymont/genericEndpoints.pvl

@@ -0,0 +1,23 @@
+class Role<T> {
+  T t;
+  int i;
+
+  T fromInt(int i);
+  int toInt(T t);
+}
+
+class A { }
+
+class B { }
+
+seq_program genericTest() {
+  endpoint a = Role<A>();
+  endpoint b = Role<B>();
+
+  requires a != b;
+  seq_run {
+    a.i := a.toInt(a.t);
+    communicate a.i -> b.i;
+    b.t := b.fromInt(b.i);
+  }
+}