Skip to content

Commit bf62883

Browse files
authored
Merge pull request #5537 from sakehl/patch-1
Update cbmc-tutorial.md
2 parents fa4569e + 51c23e3 commit bf62883

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

doc/cprover-manual/cbmc-tutorial.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -119,7 +119,7 @@ Let us have a closer look at this property and why it fails. To aid the
119119
understanding of the problem, CBMC can generate a *counterexample trace*
120120
for failed properties. To obtain this trace, run:
121121

122-
cbmc file1.c --bounds-check --trace
122+
cbmc file1.c --bounds-check --pointer-check --trace
123123

124124
CBMC then prints a counterexample trace, that is, a program trace that
125125
begins with `main` and ends in a state which violates the property. In
@@ -134,7 +134,7 @@ To simplify further processing of counterexample traces, CBMC supports XML as a
134134
possible output format.
135135

136136
```
137-
cbmc file1.c --trace --xml-ui
137+
cbmc file1.c --bounds-check --pointer-check --trace --xml-ui
138138
```
139139

140140
The specification of the XML trace output can be found here: [XML

0 commit comments

Comments
 (0)