Skip to content

Commit 3956d75

Browse files
author
Daniel Kroening
committed
manual: fix formatting of cbmc output
1 parent 8b7bcb6 commit 3956d75

File tree

1 file changed

+16
-14
lines changed

1 file changed

+16
-14
lines changed

doc/cprover-manual/properties.md

Lines changed: 16 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -203,20 +203,22 @@ goto-instrument error_example.goto error_example_replaced.goto \
203203
cbmc error_example_replaced.goto
204204
```
205205

206-
Which gets us the output
207-
208-
> ** Results:
209-
> error_example.c function api_error
210-
> [api_error.assertion.1] line 4 assertion false: FAILURE
211-
>
212-
> error_example.c function internal_error
213-
> [internal_error.assertion.1] line 5 assertion false: FAILURE
214-
>
215-
> ** 2 of 2 failed (2 iterations)
216-
> VERIFICATION FAILED
217-
218-
As opposed to the verification success we would have seen without the
219-
instrumentation step.
206+
This generates the following output:
207+
208+
```
209+
** Results:
210+
error_example.c function api_error
211+
[api_error.assertion.1] line 4 assertion false: FAILURE
212+
213+
error_example.c function internal_error
214+
[internal_error.assertion.1] line 5 assertion false: FAILURE
215+
216+
** 2 of 2 failed (2 iterations)
217+
VERIFICATION FAILED
218+
```
219+
220+
Without the instrumentation step we would have seen
221+
"VERIFICATION SUCCESSFUL".
220222

221223
The havoc option takes further parameters `globals` and `params` with this
222224
syntax: `havoc[,globals:<regex>][,params:<regex>]` (where the square brackets

0 commit comments

Comments
 (0)