Skip to content

Commit

Permalink
chore: tabs instead of spaces
Browse files Browse the repository at this point in the history
  • Loading branch information
gottschali committed Jan 29, 2025
1 parent 04809a0 commit 4d82955
Show file tree
Hide file tree
Showing 6 changed files with 20 additions and 20 deletions.
8 changes: 4 additions & 4 deletions src/addressable.md
Original file line number Diff line number Diff line change
Expand Up @@ -18,21 +18,21 @@ For a variable `b` we either write `b /*@@@*/` using an inline annotation or equ
func main() {
b /*@@@*/ := 1
// b@ := 1 // .gobra version
x := &b
x := &b
}
```

Otherwise, if we try to take the address of a non-shared variable, Gobra reports an error:
``` go
func main() {
b := 1
x := &b
x := &b
}
```
``` text
property error: got b that is not effective addressable
x := &b
^
x := &b
^
```

## Shared structs and arrays
Expand Down
2 changes: 1 addition & 1 deletion src/fractional-permissions.md
Original file line number Diff line number Diff line change
Expand Up @@ -116,7 +116,7 @@ func (p *pair) sum() (s int) {
func client() {
p := &pair{3, 5}
res := p.sum()
// @ assert p.left == 3 && p.right == 5
// @ assert p.left == 3 && p.right == 5
// @ assert res == 8
}
```
Expand Down
2 changes: 1 addition & 1 deletion src/permission-pure.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# Pure functions and permissions
Endtext# Pure functions and permissions

Recall that [pure functions](./basic-ghost-pure.md) have no side effects.
Hence, they must not leak any permissions and implicitly return all permissions mentioned in the precondition.
Expand Down
8 changes: 4 additions & 4 deletions src/permission-write.md
Original file line number Diff line number Diff line change
Expand Up @@ -64,10 +64,10 @@ func swap(x *int, y *int) {
func client() {
x := new(int)
y := new(int)
// @ assert acc(x)
// @ assert acc(y)
*x = 1
*y = 2
// @ assert acc(x)
// @ assert acc(y)
*x = 1
*y = 2
swap(x, y)
// @ assert *x == 2 // fail
// @ assert *y == 1
Expand Down
6 changes: 3 additions & 3 deletions src/self-framing.md
Original file line number Diff line number Diff line change
Expand Up @@ -72,9 +72,9 @@ However, Gobra reports an error if `acc(x)` is not held in the state.
``` go
func client() {
x := new(int)
*x = 1
// @ assert *x == 1
// @ assert acc(x) && *x == 1
*x = 1
// @ assert *x == 1
// @ assert acc(x) && *x == 1
}
```

Expand Down
14 changes: 7 additions & 7 deletions src/slices.md
Original file line number Diff line number Diff line change
Expand Up @@ -54,11 +54,11 @@ To check slicing does not panic, Gobra checks as part of the contract of the sli
We may create two overlapping slices `l` and `r` but run into a permission error:
``` go
func overlappingFail() {
s := make([]int, 3)
l := s[:2]
r := s[1:]
addToSlice(l, 1)
addToSlice(r, 1) // error
s := make([]int, 3)
l := s[:2]
r := s[1:]
addToSlice(l, 1)
addToSlice(r, 1) // error
}
```
``` go
Expand Down Expand Up @@ -129,11 +129,11 @@ This simple example shows the usage of `copy` and `append`:
``` go
s1 := []int{1, 2}
s2 := []int{3, 4, 5}

s0 := make([]int, len(s1))
copy(s0, s1 /*@, perm(1/2) @*/)
// @ assert forall i int :: {&s0[i]} {&s1[i]} 0 <= i && i < len(s0) ==> s0[i] == s1[i]

s3 := append(/*@ perm(1/2), @*/ s1, s2...)
s4 := append(/*@ perm(1/2), @*/ s0, 3, 4, 5)
// @ assert forall i int :: {&s3[i]} {&s4[i]} 0 <= i && i < len(s3) ==> s3[i] == s4[i]
Expand Down

0 comments on commit 4d82955

Please sign in to comment.