We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent d1b7069 commit 4b66d29Copy full SHA for 4b66d29
doc/cprover-manual/requires-and-ensures-clauses.md
@@ -61,7 +61,7 @@ __CPROVER_ensures((__CPROVER_return_value == SUCCESS) ==> (*out == (*a + *b)))
61
In order to determine whether _requires_ and _ensures_ clauses are a sound
62
characterization of the behavior of a function *f*, CBMC will try to check them as follows:
63
64
-1. Considers all arguments and global variables as non-determinisc values;
+1. Considers all arguments and global variables as non-deterministic values;
65
2. Assumes all preconditions specified in the `__CPROVER_requires` clauses;
66
4. Calls the implementation of function *f*;
67
5. Asserts all postconditions described in the `__CPROVER_ensures` clauses.
0 commit comments