Skip to content

Commit d1b7069

Browse files
Update doc/cprover-manual/requires-and-ensures-clauses.md
Co-authored-by: Saswat Padhi <[email protected]>
1 parent f72ef25 commit d1b7069

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

doc/cprover-manual/requires-and-ensures-clauses.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ To illustrate these two perspectives, consider the following implementation of t
4141

4242
```c
4343
int sum(uint32_t* a, uint32_t* b, uint32_t* out)
44-
/* Precondition */
44+
/* Preconditions */
4545
__CPROVER_requires(__CPROVER_is_fresh(a, sizeof(*a)))
4646
__CPROVER_requires(__CPROVER_is_fresh(b, sizeof(*b)))
4747
__CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out)))

0 commit comments

Comments
 (0)