Merge branch 'master' into meilers_carbon_missing_features_tests

src/test/resources/all/functions/linkedlists.vpr

@@ -1,6 +1,8 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
+//:: IgnoreFile(/silicon/issue/104/)
+
 // NOTES (important points are also commented in the code below)
 // (1) The definition of list(xs) precludes the case xs==null. But, without unfolding the predicate, this information is not available. This is important for e.g.,
 // showing that length increases by 1 when prepending. For now, the explicit non-nullity of the argument has been conjoined everywhere.

src/test/resources/all/sequences/sequence_incompletenesses.vpr

@@ -44,7 +44,7 @@ method colourings0(a: Array)
   slot(a,1).val := Seq(Seq(0,1)) // no red, 1 black
   assert valid(Seq(),0,false) // needed for unrolling valid
   //assert Seq(0,1)[2..] == Seq() // sequence incompleteness
-  //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/380/)
+  // // UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/380/)
   // // UnexpectedOutput(assert.failed:assertion.false, /silver/issue/80/) // fixed with diff 5 in Carbon
   assert forall j:Int :: 0 <= j && j < |slot(a,1).val| ==>
         slot(a,1).val[j] == Seq(0,1) && valid(slot(a,1).val[j],1,true)
@@ -104,7 +104,7 @@ method colourings1(a: Array)
       if(oldSoln[0] == 0) {  // therefore seq is of length >= 2
         soln := oldSoln[1 := oldSoln[1]+1] // add one to initial blacks
        // assert soln[2..] == oldSoln[2..]
-        //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/380/)
+        // // UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/380/)
         assert valid(soln,n,true) 
       } else {
         soln := Seq(0,1) ++ oldSoln
@@ -180,7 +180,7 @@ method colourings2(a: Array)
         soln := Seq(0,1) ++ oldSoln
         //assert soln[2..] == oldSoln
         assert valid(oldSoln,n-1,false)
-        //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/380/)
+        // // UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/380/)
         assert valid(soln,n,true)
       }
       slot(a,n).val := slot(a,n).val ++ Seq(soln)
@@ -271,7 +271,7 @@ method test_extend(s:Seq[Int])
 method test_extend_left(s:Seq[Int])
 {
   var ss : Seq[Int] := Seq(42) ++ s
-   //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/380/)
+   // // UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/380/)
    assert forall i:Int :: i in s ==> i in ss[1..]
 }
 
@@ -284,6 +284,6 @@ method test_append_left(s:Seq[Int], t:Seq[Int])
 method test_append_right(s:Seq[Int], t:Seq[Int])
 {
   var ss : Seq[Int] := s ++ t
-   //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/380/)
+   // // UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/380/)
   assert forall i:Int :: i in t ==> i in ss[|s|..]
 }

src/test/resources/examples/quickselect/arrays_quickselect_rec.vpr

@@ -2,6 +2,7 @@
 // http://creativecommons.org/publicdomain/zero/1.0/
 
 //:: IgnoreFile(/carbon/issue/280/)
+//:: IgnoreFile(/silicon/issue/104/)
 
 
 /* https://en.wikipedia.org/wiki/Quickselect

src/test/resources/examples/quickselect/arrays_quickselect_rec_index-shifting.vpr

@@ -2,6 +2,8 @@
 // http://creativecommons.org/publicdomain/zero/1.0/
 
 //:: IgnoreFile(/carbon/issue/280/)
+//:: IgnoreFile(/silicon/issue/104/)
+
 
 /* This version differs from arrays_quickselect_rec.vpr in so far as the
  * permutation witness pw only covers the segment of the array that is being

src/test/resources/quantifiedpermissions/issues/issue_0064.vpr

@@ -27,7 +27,7 @@ method m03(S1: Seq[Ref], S2: Set[Ref], x: Ref)
 method m04(S1: Seq[Ref], S2: Set[Ref], x: Ref)
   requires S1 == Seq(x) && S2 == Set(x)
   requires forall y: Ref :: y in S1 ==> y != null
-  //:: UnexpectedOutput(postcondition.violated:assertion.false, /silicon/issue/150/)
+  // // UnexpectedOutput(postcondition.violated:assertion.false, /silicon/issue/150/)
   // // UnexpectedOutput(postcondition.violated:assertion.false, /carbon/issue/117/)
   ensures  forall y: Ref :: y in S2 ==> y != null
 {}
@@ -44,7 +44,7 @@ method test01(s:Seq[Ref])
 {
   inhale forall x: Ref :: x in s ==> acc(x.f)
   assert forall x: Ref :: x in s ==> x != null
-  //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/64/)
+  // // UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/64/)
   // // UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/117/) // fixed with diff 8
   assert forall i: Int :: 0 <= i && i < |s| ==> s[i] != null
 }