Merge pull request #683 from viperproject/carbon_pr_457

Update tests for Carbon exhale with well-definedness change (Carbon PR viperproject/carbon#457)

src/test/resources/all/issues/carbon/0213.vpr

@@ -11,5 +11,6 @@ method test(r:Ref)
   requires P(r)
   {
       assert perm(r.next) == none
+      //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/213/)
       assert (unfolding P(r) in perm(r.next) == write)
   }

src/test/resources/all/issues/carbon/0406.vpr

@@ -0,0 +1,24 @@
+field f: Ref
+
+method m1() {
+    var y: Ref
+    var z: Ref
+    inhale acc(y.f) && acc(z.f)
+    exhale acc(y.f) && forperm x: Ref [x.f] :: x != z ==> 0/0 == 0/0
+}
+
+method m2() {
+    var x: Ref
+
+    inhale acc(x.f)
+
+    //:: ExpectedOutput(exhale.failed:division.by.zero)
+    exhale acc(x.f) && (perm(x.f) == none ==> 0/0 == 0/0)
+}
+
+method m3() {
+    var x: Ref
+
+    inhale acc(x.f)
+    exhale acc(x.f) && (perm(x.f) != none ==> 0/0 == 0/0)
+}

src/test/resources/examples/vmcai2016/linked-list-predicates.vpr

@@ -1,6 +1,8 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
+//:: IgnoreFile(/carbon/issue/280/)
+
 /*****************************************************************
  * List Nodes
  *****************************************************************/