Skip to content

Commit 41af31c

Browse files
NlightNFotisNlightNFotis
authored
Merge pull request #8093 from NlightNFotis/new_flags_on_clean
Enable default analysis flags for CBMC version 6.0+
2 parents 9459ea5 + 9747f61 commit 41af31c

File tree

48 files changed

+360
-93
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

48 files changed

+360
-93
lines changed

‎doc/man/cbmc.1

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,12 @@ cbmc \- Bounded Model Checker for C/C++ and Java programs
88

99
.B cbmc [--all-properties] \fIfile.c\fB ...
1010

11+
.B cbmc [--no-standard-checks] \fIfile.c\fB ...
12+
13+
.B cbmc [--no-standard-checks] [--pointer-check] \fIfile.c\fB ...
14+
15+
.B cbmc [--no-bounds-check] \fIfile.c\fB ...
16+
1117
.B goto-cc [-I \fIinclude-path\fB] [-c] \fIfile.c\fB [-o \fIoutfile.o\fB]
1218

1319
.B goto-instrument \fIinfile\fB \fIoutfile\fR
@@ -41,8 +47,79 @@ The usual flow is to (1) translate source into a GOTO binary using
4147
goto-cc, then (2) perform instrumentation with goto-instrument, and
4248
finally (3) perform the analysis with cbmc.
4349
.SH OPTIONS
50+
.SS "Standard Checks"
51+
From version \fB6.0\fR onwards, \fBcbmc\fR, \fBgoto-analyzer\fR and some other tools
52+
apply some checks to the program by default (called the "standard checks"), with the
53+
aim to provide a better user experience for a non-expert user of the tool. These checks are:
54+
.TP
55+
\fB\-\-pointer\-check\fR
56+
enable pointer checks
57+
.TP
58+
\fB\-\-bounds\-check\fR
59+
enable array bounds checks
60+
.TP
61+
\fB\-\-undefined\-shift\-check\fR
62+
check shift greater than bit\-width
63+
.TP
64+
\fB\-\-div\-by\-zero\-check\fR
65+
enable division by zero checks
66+
.TP
67+
\fB\-\-pointer\-primitive\-check\fR
68+
checks that all pointers in pointer primitives are valid or null
69+
.TP
70+
\fB\-\-signed\-overflow\-check\fR
71+
enable signed arithmetic over\- and underflow checks
72+
.TP
73+
\fB\-\-malloc\-may\-fail\fR
74+
allow malloc calls to return a null pointer
75+
.TP
76+
\fB\-\-malloc\-fail\-null\fR
77+
set malloc failure mode to return null
78+
.TP
79+
\fB\-\-unwinding\-assertions\fR (\fBcbmc\fR\-only)
80+
generate unwinding assertions (cannot be
81+
used with \fB\-\-cover\fR)
82+
.PP
83+
These checks can all be deactivated at once by using the \fB\-\-no\-standard\-checks\fR flag
84+
like in the header example, or individually, by prepending a \fBno\-\fR before the flag, like
85+
so:
86+
.TP
87+
\fB\-\-no\-pointer\-check\fR
88+
disable pointer checks
89+
.TP
90+
\fB\-\-no\-bounds\-check\fR
91+
disable array bounds checks
92+
.TP
93+
\fB\-\-no\-undefined\-shift\-check\fR
94+
do not perform check for shift greater than bit\-width
95+
.TP
96+
\fB\-\-no\-div\-by\-zero\-check\fR
97+
disable division by zero checks
98+
.TP
99+
\fB\-\-no\-pointer\-primitive\-check\fR
100+
do not check that all pointers in pointer primitives are valid or null
101+
.TP
102+
\fB\-\-no\-signed\-overflow\-check\fR
103+
disable signed arithmetic over\- and underflow checks
104+
.TP
105+
\fB\-\-no\-malloc\-may\-fail\fR
106+
do not allow malloc calls to fail by default
107+
.TP
108+
\fB\-\-no\-malloc\-fail\-null\fR
109+
do not set malloc failure mode to return null pointer
110+
.TP
111+
\fB\-\-no\-unwinding\-assertions\fR (\fBcbmc\fR\-only)
112+
do not generate unwinding assertions (cannot be
113+
used with \fB\-\-cover\fR)
114+
.PP
115+
If an already set flag is re-set, like calling \fB\-\-pointer\-check\fR
116+
when default checks are already on, the flag is simply ignored.
44117
.SS "Analysis options:"
45118
.TP
119+
\fB\-\-no\-standard\-checks\fR
120+
disable the standard (default) checks applied to a C/GOTO program
121+
(see above for more information)
122+
.TP
46123
\fB\-\-show\-properties\fR
47124
show the properties, but don't run analysis
48125
.TP

‎doc/man/goto-analyzer.1

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,12 @@ goto-analyzer \- Data-flow analysis for C programs and goto binaries
88

99
.B goto\-analyzer [options] file.c|file.gb
1010

11+
.B goto\-analyzer [--no-standard-checks] \fIfile.c\fB ...
12+
13+
.B goto\-analyzer [--no-standard-checks] [--pointer-check] \fIfile.c\fB ...
14+
15+
.B goto\-analyzer [--no-bounds-check] \fIfile.c\fB ...
16+
1117
.SH DESCRIPTION
1218
.B goto-analyzer
1319
is an abstract interpreter which uses the same
@@ -494,6 +500,10 @@ list loaded goto functions
494500
show the properties, but don't run analysis
495501
.SS "Program instrumentation options:"
496502
.TP
503+
\fB\-\-no\-standard\-checks\fR
504+
disable the standard (default) checks applied to a C/GOTO program
505+
(see below for more information)
506+
.TP
497507
\fB\-\-property\fR id
498508
enable selected properties only
499509
.TP
@@ -569,6 +579,73 @@ set malloc failure mode to return null
569579
.TP
570580
\fB\-\-string\-abstraction\fR
571581
track C string lengths and zero\-termination
582+
.SS "Standard Checks"
583+
From version \fB6.0\fR onwards, \fBcbmc\fR, \fBgoto-analyzer\fR and some other tools
584+
apply some checks to the program by default (called the "standard checks"), with the
585+
aim to provide a better user experience for a non-expert user of the tool. These checks are:
586+
.TP
587+
\fB\-\-pointer\-check\fR
588+
enable pointer checks
589+
.TP
590+
\fB\-\-bounds\-check\fR
591+
enable array bounds checks
592+
.TP
593+
\fB\-\-undefined\-shift\-check\fR
594+
check shift greater than bit\-width
595+
.TP
596+
\fB\-\-div\-by\-zero\-check\fR
597+
enable division by zero checks
598+
.TP
599+
\fB\-\-pointer\-primitive\-check\fR
600+
checks that all pointers in pointer primitives are valid or null
601+
.TP
602+
\fB\-\-signed\-overflow\-check\fR
603+
enable signed arithmetic over\- and underflow checks
604+
.TP
605+
\fB\-\-malloc\-may\-fail\fR
606+
allow malloc calls to return a null pointer
607+
.TP
608+
\fB\-\-malloc\-fail\-null\fR
609+
set malloc failure mode to return null
610+
.TP
611+
\fB\-\-unwinding\-assertions\fR (\fBcbmc\fR\-only)
612+
generate unwinding assertions (cannot be
613+
used with \fB\-\-cover\fR)
614+
.PP
615+
These checks can all be deactivated at once by using the \fB\-\-no\-standard\-checks\fR flag
616+
like in the header example, or individually, by prepending a \fBno\-\fR before the flag, like
617+
so:
618+
.TP
619+
\fB\-\-no\-pointer\-check\fR
620+
disable pointer checks
621+
.TP
622+
\fB\-\-no\-bounds\-check\fR
623+
disable array bounds checks
624+
.TP
625+
\fB\-\-no\-undefined\-shift\-check\fR
626+
do not perform check for shift greater than bit\-width
627+
.TP
628+
\fB\-\-no\-div\-by\-zero\-check\fR
629+
disable division by zero checks
630+
.TP
631+
\fB\-\-no\-pointer\-primitive\-check\fR
632+
do not check that all pointers in pointer primitives are valid or null
633+
.TP
634+
\fB\-\-no\-signed\-overflow\-check\fR
635+
disable signed arithmetic over\- and underflow checks
636+
.TP
637+
\fB\-\-no\-malloc\-may\-fail\fR
638+
do not allow malloc calls to fail by default
639+
.TP
640+
\fB\-\-no\-malloc\-fail\-null\fR
641+
do not set malloc failure mode to return null pointer
642+
.TP
643+
\fB\-\-no\-unwinding\-assertions\fR (\fBcbmc\fR\-only)
644+
do not generate unwinding assertions (cannot be
645+
used with \fB\-\-cover\fR)
646+
.PP
647+
If an already set flag is re-set, like calling \fB\-\-pointer\-check\fR
648+
when default checks are already on, the flag is simply ignored.
572649
.SS "Other options:"
573650
.TP
574651
\fB\-\-validate\-goto\-model\fR

‎regression/acceleration/accelerate.sh

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ is_windows=$4
1616
shift 4
1717

1818
cfile=""
19-
cbmcargs=""
19+
cbmcargs="--no-standard-checks"
2020

2121
# create the temporary directory relative to the current directory, thus
2222
# avoiding file names that start with a "/", which confuses goto-cl (Windows)

‎regression/book-examples/CMakeLists.txt

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -13,27 +13,27 @@ else()
1313
endif()
1414

1515
add_test_pl_tests(
16-
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests}
16+
"$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests}
1717
)
1818

1919
add_test_pl_profile(
2020
"book-examples-paths-lifo"
21-
"$<TARGET_FILE:cbmc> --paths lifo"
21+
"$<TARGET_FILE:cbmc> --no-standard-checks --paths lifo"
2222
"-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo;${exclude_win_broken_tests_string}"
2323
"CORE"
2424
)
2525

2626
add_test_pl_profile(
2727
"book-examples-cprover-smt2"
28-
"$<TARGET_FILE:cbmc> --cprover-smt2"
28+
"$<TARGET_FILE:cbmc> --no-standard-checks --cprover-smt2"
2929
"-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2;${exclude_win_broken_tests_string}"
3030
"CORE"
3131
)
3232

3333
# If `-X` (exclude flag) is passed, test.pl will exclude the tests matching the label following it.
3434
add_test_pl_profile(
3535
"book-examples-new-smt-backend"
36-
"$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
36+
"$<TARGET_FILE:cbmc> --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in'"
3737
"${gcc_only_string}-X;no-new-smt;-s;new-smt-backend"
3838
"CORE"
3939
)

‎regression/book-examples/Makefile

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -10,27 +10,27 @@ GCC_ONLY =
1010
endif
1111

1212
test:
13-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
13+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
1414

1515
test-cprover-smt2:
16-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" \
16+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --cprover-smt2" \
1717
-X broken-smt-backend -X thorough-smt-backend \
1818
-X broken-cprover-smt-backend -X thorough-cprover-smt-backend \
1919
-s cprover-smt2 $(GCC_ONLY)
2020

2121
test-z3:
22-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --z3" \
22+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --z3" \
2323
-X broken-smt-backend -X thorough-smt-backend \
2424
-X broken-z3-smt-backend -X thorough-z3-smt-backend \
2525
-s z3 $(GCC_ONLY)
2626

2727
test-paths-lifo:
28-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" \
28+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --paths lifo" \
2929
-X thorough-paths -X smt-backend -X paths-lifo-expected-failure \
3030
-s paths-lifo $(GCC_ONLY)
3131

3232
test-new-smt-backend:
33-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in'" \
33+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in'" \
3434
-X no-new-smt \
3535
-s new-smt-backend $(GCC_ONLY)
3636

‎regression/cbmc-concurrency/CMakeLists.txt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
if((NOT WIN32) AND (NOT APPLE))
22
add_test_pl_tests(
3-
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
3+
"$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation"
44
)
55
else()
66
add_test_pl_profile(
77
"cbmc-concurrency"
8-
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
8+
"$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation"
99
"-C;-X;pthread"
1010
"CORE"
1111
)

‎regression/cbmc-concurrency/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,10 @@ ifeq ($(filter-out OSX MSVC,$(BUILD_ENV_)),)
1010
endif
1111

1212
test:
13-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(no_pthread)
13+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(no_pthread)
1414

1515
tests.log: ../test.pl
16-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(no_pthread)
16+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(no_pthread)
1717

1818
clean:
1919
find . -name '*.out' -execdir $(RM) '{}' \;

‎regression/cbmc-cover/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
add_test_pl_tests(
2-
"$<TARGET_FILE:cbmc>"
2+
"$<TARGET_FILE:cbmc> --no-standard-checks"
33
)

‎regression/cbmc-cover/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
default: tests.log
22

33
test:
4-
@../test.pl -e -p -c ../../../src/cbmc/cbmc
4+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks"
55

66
tests.log: ../test.pl
7-
@../test.pl -e -p -c ../../../src/cbmc/cbmc
7+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks"
88

99
clean:
1010
find . -name '*.out' -execdir $(RM) '{}' \;

‎regression/cbmc-cpp/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,5 +5,5 @@ else()
55
endif()
66

77
add_test_pl_tests(
8-
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" ${gcc_only}
8+
"$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation" ${gcc_only}
99
)

‎regression/cbmc-cpp/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,10 @@ ifeq ($(BUILD_ENV_),MSVC)
88
endif
99

1010
test:
11-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(excluded_tests)
11+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(excluded_tests)
1212

1313
tests.log: ../test.pl
14-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(excluded_tests)
14+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(excluded_tests)
1515

1616
clean:
1717
find . -name '*.out' -execdir $(RM) '{}' \;

‎regression/cbmc-incr-oneloop/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
add_test_pl_tests(
2-
"perl ../timeout.pl 8 $<TARGET_FILE:cbmc> --slice-formula"
2+
"perl ../timeout.pl 8 $<TARGET_FILE:cbmc> --no-standard-checks --slice-formula"
33
)

‎regression/cbmc-incr-oneloop/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,10 +2,10 @@ default: tests.log
22

33
# Note the `perl -e` serves the purpose of providing timeout
44
test:
5-
@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --slice-formula"
5+
@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --no-standard-checks --slice-formula"
66

77
tests.log: ../test.pl
8-
@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --slice-formula"
8+
@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --no-standard-checks --slice-formula"
99

1010
clean:
1111
@$(RM) *.log

‎regression/cbmc-incr-smt2/CMakeLists.txt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
11
add_test_pl_profile(
22
"cbmc-incr-smt2-z3"
3-
"$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
3+
"$<TARGET_FILE:cbmc> --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
44
"-C;-s;new-smt-z3"
55
"CORE"
66
)
77

88
add_test_pl_profile(
99
"cbmc-incr-smt2-cvc5"
10-
"$<TARGET_FILE:cbmc> --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation"
10+
"$<TARGET_FILE:cbmc> --no-standard-checks --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation"
1111
"-C;-s;new-smt-cvc5"
1212
"CORE"
1313
)

‎regression/cbmc-incr-smt2/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,10 @@ include ../../src/common
66
test: test.z3 test.cvc5
77

88
test.z3:
9-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
9+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
1010

1111
test.cvc5:
12-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation"
12+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation"
1313

1414
tests.log: ../test.pl test
1515

‎regression/cbmc-incr/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
add_test_pl_tests(
2-
"perl ../timeout.pl 30 $<TARGET_FILE:cbmc> --incremental --magic-numbers"
2+
"perl ../timeout.pl 30 $<TARGET_FILE:cbmc> --no-standard-checks --incremental --magic-numbers"
33
)

‎regression/cbmc-incr/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
default: tests.log
22

3-
PARAM = --incremental --magic-numbers
3+
PARAM = --incremental --magic-numbers --no-standard-checks
44
# --refine --slice-formula
55

66
test:

0 commit comments

Comments
 (0)