Skip to content

Commit a9a82c7

Browse files
committed
Remove documentation of --malloc-fail-assert
This option will be deprecated, users should just stick with --pointer-check.
1 parent 74d827d commit a9a82c7

File tree

1 file changed

+2
-8
lines changed

1 file changed

+2
-8
lines changed

doc/cprover-manual/memory-primitives.md

Lines changed: 2 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -122,12 +122,10 @@ configurations:
122122
|Flag | Check |
123123
|------------------------|---------------------------------------------------|
124124
| `--malloc-fail-null` | return NULL when emulating an allocation failure |
125-
| `--malloc-fail-assert` | report a failed property upon allocation failure |
126125
| `--malloc-may-fail` | non-deterministically fail to allocate |
127126

128-
Note that the use of `--malloc-may-fail` also requires one of
129-
`--malloc-fail-null` or `--malloc-fail-assert` to be given. The following code
130-
example demonstrates the effect of these options:
127+
Note that the use of `--malloc-may-fail` also requires `--malloc-fail-null`. The
128+
following code example demonstrates the effect of these options:
131129

132130
```C
133131
int error = 0;
@@ -143,10 +141,6 @@ When running CBMC with `--malloc-fail-null --malloc-may-fail`, `p` would
143141
non-deterministically be set to `NULL`, making all branches in the above code
144142
reachable.
145143

146-
When running CBMC with `--malloc-fail-assert --malloc-may-fail`, CBMC reports a
147-
failed property instead of returning `NULL`. The `else` branch remains
148-
unreachable.
149-
150144
These malloc failure options need to be set when the C library model is added to
151145
the program. Typically this is upon invoking CBMC, but if the user has chosen to
152146
do so via \ref goto-instrument (using `goto-instrument --add-library`), then the

0 commit comments

Comments
 (0)