Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adapting tests for improved sequence, set, ... axioms in Silicon #765

Merged
merged 7 commits into from
Jan 22, 2024
Merged

Adapting tests for improved sequence, set, ... axioms in Silicon #765

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
794a7c8
Updating expected output after sequence axiom update
marcoeilers Aug 22, 2022
b25804e
Removed two more unexpected output annotations
marcoeilers Aug 22, 2022
e13fccb
Fixed test annotation
marcoeilers Aug 22, 2022
58646a4
Merge branch 'master' into meilers_silicon_seq_set_axioms
marcoeilers Sep 23, 2022
c244f9d
Merge branch 'master' into meilers_silicon_seq_set_axioms
marcoeilers Oct 17, 2023
f5d9caf
Merge branch 'master' into meilers_silicon_seq_set_axioms
marcoeilers Jan 21, 2024
db22e13
Ignore tests that randomly cause non-termination with new sequence ax…
marcoeilers Jan 21, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions src/test/resources/all/functions/linkedlists.vpr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
Expand Down
10 changes: 5 additions & 5 deletions src/test/resources/all/sequences/sequence_incompletenesses.vpr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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..]
}

Expand All @@ -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|..]
}
1 change: 1 addition & 0 deletions src/test/resources/examples/quickselect/arrays_quickselect_rec.vpr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions src/test/resources/examples/quickselect/arrays_quickselect_rec_index-shifting.vpr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions src/test/resources/quantifiedpermissions/issues/issue_0064.vpr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
{}
Expand All @@ -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
}
Expand Down
Loading