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.

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

Add opaque/reveal to Gobra #715

Merged
merged 23 commits into from
Feb 8, 2024
Merged
Changes from 1 commit
Commits
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
Next Next commit
Port fac from Viper's opaque test
dnezam committed Dec 27, 2023

Unverified

This user has not yet uploaded their public signing key.
commit f7ab65c2372e120f30370822e0bf54ff2d209bff
27 changes: 27 additions & 0 deletions src/test/resources/regressions/features/opaque/opaque-fac1.gobra
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
// Any copyright is dedicated to the Public Domain.
// http://creativecommons.org/publicdomain/zero/1.0/

package pkg
dnezam marked this conversation as resolved.
Show resolved Hide resolved

ghost
decreases i
pure func fac(i int) int {
return i <= 1 ? 1 : i * fac(i - 1)
}

ghost
decreases
func example1 (i int) int {
tmp := fac(3)
//:: ExpectedOutput(assert_error:assertion_error)
assert tmp == 6
}

ghost
decreases
func example2 (i int) int {
tmp := fac(3)
assert tmp == 3 * fac(2)
assert tmp == 3 * 2 * fac(1)
assert tmp == 6
}
16 changes: 16 additions & 0 deletions src/test/resources/regressions/features/opaque/opaque-fac1.gobra~
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
// Any copyright is dedicated to the Public Domain.
// http://creativecommons.org/publicdomain/zero/1.0/

package pkg

ghost
decreases i
pure func fac1(i int) int {
return i <= 1 ? 1 : i * fac1(i - 1)
}

ghost
decreases i
pure func fac2(i int) int {
return i <= 1 ? 1 : i * fac2(i - 1)
}
44 changes: 44 additions & 0 deletions src/test/resources/regressions/features/opaque/opaque-fac2.gobra
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
// Any copyright is dedicated to the Public Domain.
// http://creativecommons.org/publicdomain/zero/1.0/

package pkg

ghost
decreases i
opaque pure func fac(i int) int {
return i <= 1 ? 1 : i * fac(i - 1)
}

ghost
decreases
func example1 (i int) int {
tmp := fac(3)
//:: ExpectedOutput(assert_error:assertion_error)
assert tmp == 6
}

ghost
decreases
func example2 (i int) int {
tmp := fac(3)
//:: ExpectedOutput(assert_error:assertion_error)
assert tmp == 3 * fac(2)
}

ghost
decreases
func example3 (i int) int {
tmp := reveal fac(3)
assert tmp == 3 * reveal fac(2)
assert tmp == 3 * 2 * reveal fac(1)
assert tmp == 6
}

ghost
decreases
func example4 (i int) int {
tmp := reveal fac(3)
assert tmp == 3 * fac(2)
//:: ExpectedOutput(assert_error:assertion_error)
assert tmp == 3 * 2 * reveal fac(1)
}
11 changes: 11 additions & 0 deletions src/test/resources/regressions/features/opaque/opaque-fac2.gobra~
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
//:: ExpectedOutput(assert_error:assertion_error)
assert tmp == 6
}

ghost
decreases i
func example2 (i int) int {
tmp := fac(3)
//:: ExpectedOutput(assert_error:assertion_error)
assert tmp == 3 * fac(2)
}
53 changes: 53 additions & 0 deletions src/test/resources/regressions/features/opaque/opaque-fac3.gobra
Original file line number Diff line number Diff line change
@@ -0,0 +1,53 @@
// Any copyright is dedicated to the Public Domain.
// http://creativecommons.org/publicdomain/zero/1.0/

package pkg

ghost
decreases
opaque pure func fac(i int) int {
return i <= 1 ? 1 : i * (reveal fac(i - 1))
}

ghost
decreases
func example1 (i int) int {
tmp := fac(3)
//:: ExpectedOutput(assert_error:assertion_error)
assert tmp == 6
}

ghost
decreases
func example2 (i int) int {
tmp := fac(3)
//:: ExpectedOutput(assert_error:assertion_error)
assert tmp == 3 * fac(2)
}

ghost
decreases
func example3 (i int) int {
tmp := reveal fac(3)
assert tmp == 3 * reveal fac(2)
assert tmp == 3 * 2 * reveal fac(1)
assert tmp == 6
}

ghost
decreases
func example4 (i int) int {
tmp := reveal fac(3)
assert tmp == 3 * fac(2)
//:: ExpectedOutput(assert_error:assertion_error)
assert tmp == 3 * 2 * reveal fac(1)
}

ghost
decreases
func example5 (i int) int {
tmp := reveal fac(3)
//:: ExpectedOutput(assert_error:assertion_error)
assert tmp == 6
}

44 changes: 44 additions & 0 deletions src/test/resources/regressions/features/opaque/opaque-fac3.gobra~
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
// Any copyright is dedicated to the Public Domain.
// http://creativecommons.org/publicdomain/zero/1.0/

package pkg

ghost
decreases i
opaque pure func fac(i int) int {
return i <= 1 ? 1 : i * (reveal fac(i - 1))
}

ghost
decreases i
func example1 (i int) int {
tmp := fac(3)
//:: ExpectedOutput(assert_error:assertion_error)
assert tmp == 6
}

ghost
decreases i
func example2 (i int) int {
tmp := fac(3)
//:: ExpectedOutput(assert_error:assertion_error)
assert tmp == 3 * fac(2)
}

ghost
decreases i
func example3 (i int) int {
tmp := reveal fac(3)
assert tmp == 3 * reveal fac(2)
assert tmp == 3 * 2 * reveal fac(1)
assert tmp == 6
}

ghost
decreases i
func example4 (i int) int {
tmp := reveal fac(3)
assert tmp == 3 * fac(2)
//:: ExpectedOutput(assert_error:assertion_error)
assert tmp == 3 * 2 * reveal fac(1)
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
// Any copyright is dedicated to the Public Domain.
// http://creativecommons.org/publicdomain/zero/1.0/

package pkg

decreases i
pure func fac1(i int) int {
return i <= i ? 1 : i * fac1(i - 1)
}