Skip to content

Commit 57d5c97

Browse files
committed
Fixes typo in assigns clause manual
Signed-off-by: Felipe R. Monteiro <[email protected]>
1 parent 4e21c22 commit 57d5c97

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

doc/cprover-manual/contracts-assigns.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -114,7 +114,7 @@ Clauses](contracts-requires-and-ensures.md) - Replacement section, and it will a
114114
non-deterministic assignments for each object listed in the `__CPROVER_assigns`
115115
clause. Since these objects might be modified by the function, CBMC uses
116116
non-deterministic assignments to havoc them and restrict their values only by
117-
assuming the postconditions (i.e., requires clauses).
117+
assuming the postconditions (i.e., ensures clauses).
118118

119119
In our example, consider that a function `foo` may call `sum`.
120120

0 commit comments

Comments
 (0)