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 441a249 commit 4efe207Copy full SHA for 4efe207
doc/cprover-manual/cbmc-tutorial.md
@@ -216,7 +216,7 @@ given as a command line argument:
216
cbmc binsearch.c --function binsearch --unwind 6 --bounds-check --unwinding-assertions
217
```
218
219
-CBMC verifies that verifies the array accesses are within the bounds;
+CBMC verifies that the array accesses are within the bounds;
220
note that this actually depends on the result of the right shift. In
221
addition, as CBMC is given the option `--unwinding-assertions`, it also
222
checks that enough unwinding is done, i.e., it proves a run-time bound.
0 commit comments