File tree Expand file tree Collapse file tree 1 file changed +4
-3
lines changed Expand file tree Collapse file tree 1 file changed +4
-3
lines changed Original file line number Diff line number Diff line change @@ -132,9 +132,10 @@ The goto-instrument program supports these checks:
132
132
As all of these checks apply across the entire input program, we may wish to
133
133
disable them for selected statements in the program. For example, unsigned
134
134
overflows can be expected and acceptable in certain instructions even when
135
- elsewhere we do not expect them. To selectively disable automatically generated
136
- properties use `#pragma CPROVER check disable "<name_of_check>"`, which remains
137
- in effect until a `#pragma CPROVER check pop` (to re-enable all properties
135
+ elsewhere we do not expect them. As of version 5.12, CBMC supports selectively
136
+ disabling automatically generated properties. To disable property generation,
137
+ use `#pragma CPROVER check disable "<name_of_check>"`, which remains in effect
138
+ until a `#pragma CPROVER check pop` (to re-enable all properties
138
139
disabled before or since the last `#pragma CPROVER check push`) is provided.
139
140
For example, for unsigned overflow checks, use
140
141
```
You can’t perform that action at this time.
0 commit comments