File tree Expand file tree Collapse file tree 5 files changed +10
-9
lines changed Expand file tree Collapse file tree 5 files changed +10
-9
lines changed Original file line number Diff line number Diff line change @@ -102,8 +102,8 @@ do not check that all pointers in pointer primitives are valid or null
102
102
\fB \-\- no \- signed \- overflow \- check \fR
103
103
disable signed arithmetic over\- and underflow checks
104
104
.TP
105
- \fB \-\- no \- malloc \- fail \fR
106
- Do not allow malloc calls to fail by default.
105
+ \fB \-\- no \- malloc \- may \- fail \fR
106
+ do not allow malloc calls to fail by default
107
107
.TP
108
108
\fB \-\- no \- unwinding \- assertions \fR (\fB cbmc \fR \- only)
109
109
do not generate unwinding assertions (cannot be
Original file line number Diff line number Diff line change @@ -634,8 +634,8 @@ do not check that all pointers in pointer primitives are valid or null
634
634
\fB \-\- no \- signed \- overflow \- check \fR
635
635
disable signed arithmetic over\- and underflow checks
636
636
.TP
637
- \fB \-\- no \- malloc \- fail \fR
638
- Do not allow malloc calls to fail by default.
637
+ \fB \-\- no \- malloc \- may \- fail \fR
638
+ do not allow malloc calls to fail by default
639
639
.TP
640
640
\fB \-\- no \- unwinding \- assertions \fR (\fB cbmc \fR \- only)
641
641
do not generate unwinding assertions (cannot be
Original file line number Diff line number Diff line change @@ -697,8 +697,8 @@ set malloc failure mode to assert\-then\-assume
697
697
\fB \-\- malloc \- fail \- null \fR
698
698
set malloc failure mode to return null
699
699
.TP
700
- \fB \-\- no \- malloc \- fail \fR
701
- Do not allow malloc calls to fail by default.
700
+ \fB \-\- no \- malloc \- may \- fail \fR
701
+ do not allow malloc calls to fail by default
702
702
.TP
703
703
\fB \-\- string \- abstraction \fR
704
704
track C string lengths and zero\- termination
Original file line number Diff line number Diff line change @@ -1130,7 +1130,7 @@ bool configt::set(const cmdlinet &cmdline)
1130
1130
{
1131
1131
ansi_c.malloc_may_fail = true ;
1132
1132
}
1133
- if (cmdline.isset (" no-malloc-fail" ))
1133
+ if (cmdline.isset (" no-malloc-may- fail" ))
1134
1134
{
1135
1135
ansi_c.malloc_may_fail = false ;
1136
1136
ansi_c.malloc_failure_mode = ansi_ct::malloc_failure_mode_none;
Original file line number Diff line number Diff line change @@ -70,15 +70,16 @@ class symbol_table_baset;
70
70
" {y--no-library} \t disable built-in abstract C library\n "
71
71
72
72
#define OPT_CONFIG_LIBRARY \
73
- " (malloc-fail-assert)(malloc-fail-null)(malloc-may-fail)(no-malloc-fail)" \
73
+ " (malloc-fail-assert)(malloc-fail-null)(malloc-may-fail)" \
74
+ " (no-malloc-may-fail)" \
74
75
" (string-abstraction)"
75
76
76
77
#define HELP_CONFIG_LIBRARY \
77
78
" {y--malloc-may-fail} \t allow malloc calls to return a null pointer\n " \
79
+ " {y--no-malloc-may-fail} \t disable potential malloc failure\n " \
78
80
" {y--malloc-fail-assert} \t " \
79
81
" set malloc failure mode to assert-then-assume\n " \
80
82
" {y--malloc-fail-null} \t set malloc failure mode to return null\n " \
81
- " {y--no-malloc-fail} \t Disable potential malloc failure.\n " \
82
83
" {y--string-abstraction} \t track C string lengths and zero-termination\n "
83
84
84
85
#define OPT_CONFIG_JAVA " (classpath)(cp)(main-class)"
You can’t perform that action at this time.
0 commit comments