Merge branch 'master' into meilers_fix_803

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/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
+}