Skip to content

Commit a69540e

Browse files
authored
Merge pull request #7455 from diffblue/contract-doco-fixes
Fixed documentation typos
2 parents fbb702f + 6b733fe commit a69540e

File tree

2 files changed

+2
-1
lines changed

2 files changed

+2
-1
lines changed

src/goto-instrument/contracts/doc/user/contracts-assigns.md

+1
Original file line numberDiff line numberDiff line change
@@ -241,6 +241,7 @@ int main() {
241241
vec_clear(vec);
242242
}
243243
```
244+
244245
---
245246
246247
```c

src/goto-instrument/contracts/doc/user/contracts-requires-ensures.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ the conjunction of the _ensures_ clauses, or `true` if none are specified.
2929
Both _requires_ clauses and _ensures_ clauses take a Boolean expression over the
3030
arguments of a function and/or global variables. The expression can include
3131
calls to CBMC built-in functions, to
32-
[Memory Predicates](@ref contracts-memory-predicates)) or to
32+
[Memory Predicates](@ref contracts-memory-predicates) or to
3333
[function pointer predicates](@ref contracts-function-pointer-predicates).
3434
User-defined functions can also be called inside _requires_ clauses as long as
3535
they are deterministic and do not have any side-effects

0 commit comments

Comments
 (0)