From 51c23e3108d9a7051af0d13ad86cc1f01eff0f3b Mon Sep 17 00:00:00 2001 From: Lars Date: Wed, 21 Oct 2020 14:50:27 +0200 Subject: [PATCH] Update cbmc-tutorial.md The commands need the "--pointer-check" argument. --- doc/cprover-manual/cbmc-tutorial.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/cprover-manual/cbmc-tutorial.md b/doc/cprover-manual/cbmc-tutorial.md index 2c1ab33510d..6beee073154 100644 --- a/doc/cprover-manual/cbmc-tutorial.md +++ b/doc/cprover-manual/cbmc-tutorial.md @@ -119,7 +119,7 @@ Let us have a closer look at this property and why it fails. To aid the understanding of the problem, CBMC can generate a *counterexample trace* for failed properties. To obtain this trace, run: - cbmc file1.c --bounds-check --trace + cbmc file1.c --bounds-check --pointer-check --trace CBMC then prints a counterexample trace, that is, a program trace that 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 possible output format. ``` - cbmc file1.c --trace --xml-ui + cbmc file1.c --bounds-check --pointer-check --trace --xml-ui ``` The specification of the XML trace output can be found here: [XML