Skip to content

Commit

Permalink
add witness of bug
Browse files Browse the repository at this point in the history
  • Loading branch information
jcp19 committed Feb 5, 2025
1 parent 1d208a9 commit d90c9ff
Showing 1 changed file with 17 additions and 0 deletions.
17 changes: 17 additions & 0 deletions src/test/resources/regressions/issues/000815.gobra
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
// Any copyright is dedicated to the Public Domain.
// http://creativecommons.org/publicdomain/zero/1.0/

package issue815

type cell struct {
value int
}

pure
requires acc(c)
//:: ExpectedOutput(type_error)
ensures r == old(c.value)
decreases
func read(c *cell) (r int) {
return c.value
}

0 comments on commit d90c9ff

Please sign in to comment.