@@ -7,6 +7,11 @@ predicate falze()
77 false
88}
99
10+ predicate tru()
11+ {
12+ true
13+ }
14+
1015method test_unfold(){
1116 //:: ExpectedOutput(unfold.failed:permission.not.positive)
1217 unfold acc(falze(), none)
@@ -16,9 +21,9 @@ method test_unfold(){
1621method test_unfold_unknown(p: Perm){
1722 assume p >= none
1823 //:: ExpectedOutput(unfold.failed:permission.not.positive)
24+ //:: ExpectedOutput(unfold.failed:insufficient.permission)
25+ //:: MissingOutput(unfold.failed:insufficient.permission, /Silicon/issue/34/)
1926 unfold acc(falze(), p)
20- //:: ExpectedOutput(assert.failed:assertion.false)
21- //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/34/)
2227 assert false
2328}
2429
@@ -30,18 +35,18 @@ method test_unfolding(){
3035method test_unfolding_unknown(p: Perm){
3136 assume p >= none
3237 //:: ExpectedOutput(assert.failed:permission.not.positive)
33- //:: ExpectedOutput(assert.failed:assertion.false )
34- //:: MissingOutput(assert.failed:assertion.false , /Silicon/issue/34/)
38+ //:: ExpectedOutput(assert.failed:insufficient.permission )
39+ //:: MissingOutput(assert.failed:insufficient.permission , /Silicon/issue/34/)
3540 assert unfolding acc(falze(), p) in false
3641}
3742
3843method test_fold(){
3944 //:: ExpectedOutput(fold.failed:permission.not.positive)
40- fold acc(falze (), none)
45+ fold acc(tru (), none)
4146}
4247
4348method test_fold_unknown(p: Perm){
4449 assume p >= none
4550 //:: ExpectedOutput(fold.failed:permission.not.positive)
46- fold acc(falze (), p)
51+ fold acc(tru (), p)
4752}
0 commit comments