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.
2 parents 441a249 + 4efe207 commit 5fd8562Copy full SHA for 5fd8562
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