Merge branch 'master' into meilers_dont_count_requires_as_pre

src/main/scala/viper/silver/ast/utility/Expressions.scala

@@ -175,6 +175,12 @@ object Expressions {
     case e: Exp => e
   }
 
+  def containsPermissionIntrospection(e: Exp): Boolean = e.exists {
+    case _: CurrentPerm => true
+    case _: ForPerm => true
+    case _ => false
+  }
+
   // note: dependency on program for looking up function preconditions
   def proofObligations(e: Exp): (Program => Seq[Exp]) = (prog: Program) => {
     e.reduceTree[Seq[Exp]] {

src/test/resources/all/annotation/annotationProverArgs.vpr

@@ -0,0 +1,31 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// The errors marked in this file are expected only due to the proverArgs annotation, since the properties actually
+// hold, but Z3 should not be able to prove that due to the non-linear arithmetic setting.
+// We use UnexpectedOutput annotations to mark that they're not actual errors, and that Carbon (which currently does
+// not support the proverArgs annotation) should not report them.
+
+method m1(i: Int, i2: Int)
+    requires i >= 0
+    requires i2 >= 0
+{
+    assert i * i2 >= 0
+}
+
+@proverArgs("smt.arith.nl=false")
+method m2(i: Int, i2: Int)
+    requires i >= 0
+    requires i2 >= 0
+{
+    //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/000/)
+    assert i * i2 >= 0
+}
+
+@proverArgs("smt.arith.nl=true")
+method m3(i: Int, i2: Int)
+    requires i >= 0
+    requires i2 >= 0
+{
+    assert i * i2 >= 0
+}

src/test/resources/all/issues/silicon/0844.vpr

@@ -0,0 +1,77 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+method main1(tid: Int, n: Int, x0: Array, x1: Array, i: Int)
+  requires x0 != x1
+  requires alen(x0) == n && alen(x1) == n
+  requires (forall j: Int :: { hide0(x0,n,j) }
+          0 <= j && j < n ==> acc(hide0(x0,n,j), write)
+  )
+  requires (forall j: Int ::
+          { hide1(x1,n,j) }
+          0 <= j && j < n ==> acc(hide1(x1,n,j), 1/2)
+  )
+  requires (forall j: Int :: { hide0(x0,n,j) }
+          0 <= j && j < n ==> (unfolding hide0(x0,n,j) in aloc(x0, j).int) == 0)
+
+  requires i >= 0 && i < n
+{
+  //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/517/)
+  assert (forall j: Int :: { hide0(x0,n,j) }
+      0 <= j && j < n ==>
+      (unfolding hide0(x0,n,j) in aloc(x0, j).int) == 0)
+
+  unfold acc(hide1(x1, n, i),1/2)
+  fold acc(hide1(x1, n, i),1/2)
+
+  //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/517/)
+  assert (forall j: Int :: { hide0(x0,n,j) }
+      0 <= j && j < n ==>
+      (unfolding hide0(x0,n,j) in aloc(x0, j).int) == 0)
+}
+
+
+////////////////////////// Other functions
+domain Array  {
+
+  function array_loc(a: Array, i: Int): Ref
+
+  function alen(a: Array): Int
+
+  function loc_inv_1(loc: Ref): Array
+
+  function loc_inv_2(loc: Ref): Int
+
+  axiom {
+    (forall a: Array, i: Int ::
+      { array_loc(a, i) }
+      loc_inv_1(array_loc(a, i)) == a && loc_inv_2(array_loc(a, i)) == i)
+  }
+
+  axiom {
+    (forall a: Array :: { alen(a) } alen(a) >= 0)
+  }
+}
+
+field int: Int
+
+predicate hide0(x: Array, n: Int, i: Int) {
+  n > 0 && i >= 0 && i < n && alen(x) == n &&
+  acc(aloc(x, i).int, write)
+}
+
+predicate hide1(x: Array, n: Int, i: Int) {
+  n > 0 && i >= 0 && i < n && alen(x) == n &&
+  acc(aloc(x, i).int, write)
+}
+
+
+function aloc(a: Array, i: Int): Ref
+  requires 0 <= i
+  requires i < alen(a)
+  decreases
+  ensures loc_inv_1(result) == a
+  ensures loc_inv_2(result) == i
+{
+  array_loc(a, i)
+}

src/test/resources/all/issues/silicon/0845.vpr

@@ -0,0 +1,78 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+method main1(tid: Int, n: Int, x0: Array, x1: Array)
+  requires 10 < n
+  requires alen(x0) == n
+  requires (forall i: Int ::
+    {hide0(x0, n, i)}
+    0 <= i && i < n ==> acc(hide0(x0, n, i), write) )
+  requires (forall j: Int ::
+          { get0(x0, n, j) }
+          0 <= j && j < n ==>
+          get0(x0, n, j) == 0)
+{
+  assert get0(x0, n, 0) == 0
+}
+
+///////////////////////////
+
+domain Array  {
+
+  function array_loc(a: Array, i: Int): Ref
+
+  function alen(a: Array): Int
+
+  function loc_inv_1(loc: Ref): Array
+
+  function loc_inv_2(loc: Ref): Int
+
+  axiom {
+    (forall a: Array, i: Int ::
+      { array_loc(a, i) }
+      loc_inv_1(array_loc(a, i)) == a && loc_inv_2(array_loc(a, i)) == i)
+  }
+
+  axiom {
+    (forall a: Array :: { alen(a) } alen(a) >= 0)
+  }
+}
+
+field int: Int
+
+predicate hide0(x: Array, n: Int, i: Int) {
+  n > 0 && i >= 0 && i < n && alen(x) == n &&
+  acc(aloc(x, i).int, write)
+}
+
+function get0(x: Array, n: Int, i: Int): Int
+  requires 0 <= i && i < n
+  requires acc(hide0(x, n, i), write)
+  ensures result == unfolding acc(hide0(x,n, i), write) in aloc(x, i).int
+{
+  unfolding acc(hide0(x, n, i), write) in aloc(x, i).int
+}
+
+predicate hide1(x: Array, n: Int, i: Int) {
+  n > 0 && i >= 0 && i < n && alen(x) == n &&
+  acc(aloc(x, i).int, write)
+}
+
+function get1(x: Array, n: Int, i: Int): Int
+  requires 0 <= i && i < n
+  requires acc(hide1(x, n, i), wildcard)
+  ensures result == unfolding acc(hide1(x,n, i), wildcard) in aloc(x, i).int
+{
+  unfolding acc(hide1(x, n, i), wildcard) in aloc(x, i).int
+}
+
+
+function aloc(a: Array, i: Int): Ref
+  requires 0 <= i
+  requires i < alen(a)
+  decreases
+  ensures loc_inv_1(result) == a
+  ensures loc_inv_2(result) == i
+{
+  array_loc(a, i)
+}

src/test/resources/all/issues/silicon/0851.vpr

@@ -0,0 +1,25 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field v: Int
+
+field r: Ref
+
+field l: Ref
+
+function fun01(x: Ref, b1: Bool, b2: Bool): Int
+  requires acc(x.v, 1 / 3)
+  requires acc(x.v, (b1 ? 1 / 3 : none))
+  requires acc(x.v, (b2 ? 1 / 3 : none))
+{
+  x.v
+}
+
+method test01(x: Ref, b1: Bool, b2: Bool)
+  requires acc(x.v, write)
+{
+  x.v := 4
+  assert fun01(x, b2, b1) == 4
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert false
+}

src/test/resources/wands/regression/conditionals2.vpr

@@ -19,7 +19,6 @@ method test5a(x: Ref)
     //                       x.g |-> tg' # tf'' ? w : n
 
   //:: ExpectedOutput(assert.failed:insufficient.permission)
-  //:: MissingOutput(assert.failed:insufficient.permission, /silicon/issue/307/)
   assert acc(x.g, 1/1000)
 }