Update test annotations

src/test/resources/all/heap-dependent_triggers/triggerFoldPackage.vpr

@@ -12,7 +12,7 @@ method m1(xs: Set[Ref], y: Ref, zs: Seq[Ref]) {
     assume z in zs
     assume !(z in xs)
     package acc(z.f) --* acc(y.f)
-    //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/000/)
+
     //:: ExpectedOutput(assert.failed:assertion.false)
     assert z != y
 }

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

@@ -0,0 +1,82 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+domain ShStruct2[T0, T1]  {
+
+  function ShStructget1of2(x: ShStruct2[T0, T1]): T1
+
+  function ShStructget0of2(x: ShStruct2[T0, T1]): T0
+
+  function ShStructrev1of2(v1: T1): ShStruct2[T0, T1]
+
+  function ShStructrev0of2(v0: T0): ShStruct2[T0, T1]
+
+  axiom {
+    (forall x: ShStruct2[T0, T1] ::
+      { (ShStructget1of2(x): T1) }
+      (ShStructrev1of2((ShStructget1of2(x): T1)): ShStruct2[T0, T1]) == x)
+  }
+
+  axiom {
+    (forall x: ShStruct2[T0, T1] ::
+      { (ShStructget0of2(x): T0) }
+      (ShStructrev0of2((ShStructget0of2(x): T0)): ShStruct2[T0, T1]) == x)
+  }
+}
+
+field Intint$$$$_E_$$$: Int
+
+// decreases
+function witness_4e2a3fe_F(P0_PI0: Int): ShStruct2[Ref, Ref]
+    ensures witness_rev(result) == P0_PI0
+
+function witness_rev(s: ShStruct2[Ref, Ref]): Int
+
+
+predicate SharedInv_4e2a3fe_F() {
+  (forall i_V0: Int ::
+    { (ShStructget0of2(witness_4e2a3fe_F(i_V0)): Ref) }
+    true && (let fn$$0 == (witness_4e2a3fe_F(i_V0)) in true) ==>
+    acc((ShStructget0of2(witness_4e2a3fe_F(i_V0)): Ref).Intint$$$$_E_$$$, 1 /
+    2)) &&
+  (forall i_V0: Int ::
+    { (ShStructget1of2(witness_4e2a3fe_F(i_V0)): Ref) }
+    true && (let fn$$0 == (witness_4e2a3fe_F(i_V0)) in true) ==>
+    acc((ShStructget1of2(witness_4e2a3fe_F(i_V0)): Ref).Intint$$$$_E_$$$, 1 /
+    2))
+}
+
+method processRequest_4e2a3fe_F(id_V0: Int)
+  requires (let fn$$0 ==
+      (witness_4e2a3fe_F(id_V0)) in
+      acc((ShStructget0of2(fn$$0): Ref).Intint$$$$_E_$$$, 1 / 2) &&
+      acc((ShStructget1of2(fn$$0): Ref).Intint$$$$_E_$$$, 1 / 2) &&
+       true
+      )
+  requires acc(SharedInv_4e2a3fe_F(), write)
+{
+
+  // decl id_V0_CN0: int°°
+  {
+    var id_V0_CN0: Int
+
+
+
+    // init id_V0_CN0
+    inhale id_V0_CN0 == 0
+
+    // id_V0_CN0 = id_V0
+    id_V0_CN0 := id_V0
+
+    // decl
+
+    // unfold acc(SharedInv_4e2a3fe_F())
+    unfold acc(SharedInv_4e2a3fe_F(), write)
+
+    // assert false
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+    label returnLabel
+  }
+}