-
Notifications
You must be signed in to change notification settings - Fork 40
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'master' into meilers_fix_803
- Loading branch information
Showing
3 changed files
with
156 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,77 @@ | ||
// Any copyright is dedicated to the Public Domain. | ||
// http://creativecommons.org/publicdomain/zero/1.0/ | ||
|
||
method main1(tid: Int, n: Int, x0: Array, x1: Array, i: Int) | ||
requires x0 != x1 | ||
requires alen(x0) == n && alen(x1) == n | ||
requires (forall j: Int :: { hide0(x0,n,j) } | ||
0 <= j && j < n ==> acc(hide0(x0,n,j), write) | ||
) | ||
requires (forall j: Int :: | ||
{ hide1(x1,n,j) } | ||
0 <= j && j < n ==> acc(hide1(x1,n,j), 1/2) | ||
) | ||
requires (forall j: Int :: { hide0(x0,n,j) } | ||
0 <= j && j < n ==> (unfolding hide0(x0,n,j) in aloc(x0, j).int) == 0) | ||
|
||
requires i >= 0 && i < n | ||
{ | ||
//:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/517/) | ||
assert (forall j: Int :: { hide0(x0,n,j) } | ||
0 <= j && j < n ==> | ||
(unfolding hide0(x0,n,j) in aloc(x0, j).int) == 0) | ||
|
||
unfold acc(hide1(x1, n, i),1/2) | ||
fold acc(hide1(x1, n, i),1/2) | ||
|
||
//:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/517/) | ||
assert (forall j: Int :: { hide0(x0,n,j) } | ||
0 <= j && j < n ==> | ||
(unfolding hide0(x0,n,j) in aloc(x0, j).int) == 0) | ||
} | ||
|
||
|
||
////////////////////////// Other functions | ||
domain Array { | ||
|
||
function array_loc(a: Array, i: Int): Ref | ||
|
||
function alen(a: Array): Int | ||
|
||
function loc_inv_1(loc: Ref): Array | ||
|
||
function loc_inv_2(loc: Ref): Int | ||
|
||
axiom { | ||
(forall a: Array, i: Int :: | ||
{ array_loc(a, i) } | ||
loc_inv_1(array_loc(a, i)) == a && loc_inv_2(array_loc(a, i)) == i) | ||
} | ||
|
||
axiom { | ||
(forall a: Array :: { alen(a) } alen(a) >= 0) | ||
} | ||
} | ||
|
||
field int: Int | ||
|
||
predicate hide0(x: Array, n: Int, i: Int) { | ||
n > 0 && i >= 0 && i < n && alen(x) == n && | ||
acc(aloc(x, i).int, write) | ||
} | ||
|
||
predicate hide1(x: Array, n: Int, i: Int) { | ||
n > 0 && i >= 0 && i < n && alen(x) == n && | ||
acc(aloc(x, i).int, write) | ||
} | ||
|
||
|
||
function aloc(a: Array, i: Int): Ref | ||
requires 0 <= i | ||
requires i < alen(a) | ||
decreases | ||
ensures loc_inv_1(result) == a | ||
ensures loc_inv_2(result) == i | ||
{ | ||
array_loc(a, i) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,78 @@ | ||
// Any copyright is dedicated to the Public Domain. | ||
// http://creativecommons.org/publicdomain/zero/1.0/ | ||
|
||
method main1(tid: Int, n: Int, x0: Array, x1: Array) | ||
requires 10 < n | ||
requires alen(x0) == n | ||
requires (forall i: Int :: | ||
{hide0(x0, n, i)} | ||
0 <= i && i < n ==> acc(hide0(x0, n, i), write) ) | ||
requires (forall j: Int :: | ||
{ get0(x0, n, j) } | ||
0 <= j && j < n ==> | ||
get0(x0, n, j) == 0) | ||
{ | ||
assert get0(x0, n, 0) == 0 | ||
} | ||
|
||
/////////////////////////// | ||
|
||
domain Array { | ||
|
||
function array_loc(a: Array, i: Int): Ref | ||
|
||
function alen(a: Array): Int | ||
|
||
function loc_inv_1(loc: Ref): Array | ||
|
||
function loc_inv_2(loc: Ref): Int | ||
|
||
axiom { | ||
(forall a: Array, i: Int :: | ||
{ array_loc(a, i) } | ||
loc_inv_1(array_loc(a, i)) == a && loc_inv_2(array_loc(a, i)) == i) | ||
} | ||
|
||
axiom { | ||
(forall a: Array :: { alen(a) } alen(a) >= 0) | ||
} | ||
} | ||
|
||
field int: Int | ||
|
||
predicate hide0(x: Array, n: Int, i: Int) { | ||
n > 0 && i >= 0 && i < n && alen(x) == n && | ||
acc(aloc(x, i).int, write) | ||
} | ||
|
||
function get0(x: Array, n: Int, i: Int): Int | ||
requires 0 <= i && i < n | ||
requires acc(hide0(x, n, i), write) | ||
ensures result == unfolding acc(hide0(x,n, i), write) in aloc(x, i).int | ||
{ | ||
unfolding acc(hide0(x, n, i), write) in aloc(x, i).int | ||
} | ||
|
||
predicate hide1(x: Array, n: Int, i: Int) { | ||
n > 0 && i >= 0 && i < n && alen(x) == n && | ||
acc(aloc(x, i).int, write) | ||
} | ||
|
||
function get1(x: Array, n: Int, i: Int): Int | ||
requires 0 <= i && i < n | ||
requires acc(hide1(x, n, i), wildcard) | ||
ensures result == unfolding acc(hide1(x,n, i), wildcard) in aloc(x, i).int | ||
{ | ||
unfolding acc(hide1(x, n, i), wildcard) in aloc(x, i).int | ||
} | ||
|
||
|
||
function aloc(a: Array, i: Int): Ref | ||
requires 0 <= i | ||
requires i < alen(a) | ||
decreases | ||
ensures loc_inv_1(result) == a | ||
ensures loc_inv_2(result) == i | ||
{ | ||
array_loc(a, i) | ||
} |