Skip to content

Enable default analysis flags for CBMC version 6.0+ #8093

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 39 commits into from
Dec 13, 2023
Merged
Changes from 1 commit
Commits
Show all changes
39 commits
Select commit Hold shift + click to select a range
3cea665
Enable standard checks in CBMC
NlightNFotis Dec 5, 2023
457b953
Add --no-standard-checks to regression/cbmc runner scripts
NlightNFotis Dec 5, 2023
4435c12
Add --no-standard-checks to regression/cbmc-incr-smt2 runner scripts
NlightNFotis Dec 5, 2023
8b54e10
Add --no-standard-checks to regression/cbmc-shadow-memory runner scripts
NlightNFotis Dec 5, 2023
1d791d2
Add --no-standard-checks to regression/cbmc-with-incr runner scripts
NlightNFotis Dec 5, 2023
f277a9f
Add --no-standard-checks to regression/cbmc-primitives runner scripts
NlightNFotis Dec 5, 2023
161321f
Add --no-standard-checks to regression/cbmc-library runner scripts
NlightNFotis Dec 5, 2023
aaf2b8d
Add --no-standard-checks to regression/book-examples runner scripts
NlightNFotis Dec 5, 2023
d1cc469
Add --no-standard-checks to regression/cbmc-concurrency runner scripts
NlightNFotis Dec 5, 2023
cf4269d
Add --no-standard-checks to regression/cbmc-cover runner scripts
NlightNFotis Dec 5, 2023
622440c
Add --no-standard-checks to regression/cbmc-cpp runner scripts
NlightNFotis Dec 5, 2023
014a33c
Add --no-standard-checks to regression/cbmc-incr runner scripts
NlightNFotis Dec 5, 2023
2b6446e
Add --no-standard-checks to regression/cbmc-incr-oneloop test runner …
NlightNFotis Dec 5, 2023
f79b5bc
Add --no-standard-checks to regression/cbmc-sequentialization test ru…
NlightNFotis Dec 5, 2023
5f43f53
Fix issue with non-null-terminated string in shadow-memory regression…
NlightNFotis Dec 6, 2023
1f577e7
Add default options to goto-analyzer
NlightNFotis Dec 6, 2023
ce65686
Add --no-standard-checks to regression/goto-analyzer test runner scripts
NlightNFotis Dec 6, 2023
5f17296
Add --no-standard-checks to goto-analyzer-simplify runner scripts
NlightNFotis Dec 6, 2023
56e9783
Add --no-standard-checks to regression/goto-instrument test runner
NlightNFotis Dec 6, 2023
8d70395
Rework handling of `malloc-may-fail`.
NlightNFotis Dec 7, 2023
1d7d4cf
Add missing positive checks back into goto-instrument
NlightNFotis Dec 8, 2023
7e38518
Add --no-standard-checks to regression/goto-cc-cbmc test runner script
NlightNFotis Dec 8, 2023
81c73d0
Add --no-standard-checks to regression/acceleration test runner script
NlightNFotis Dec 8, 2023
bc9ae9b
Add --no-standard-checks to regresion/contracts-dfcc test runner script
NlightNFotis Dec 8, 2023
b90ea03
Add --no-standard-checks to regression/contracts test runner script
NlightNFotis Dec 8, 2023
7d65934
Add --no-standard-checks to regression/goto-synthesiser test runner s…
NlightNFotis Dec 8, 2023
0d19437
Add --no-standard-checks to regression/goto-harness test runner script
NlightNFotis Dec 8, 2023
1f81854
Add --no-standard-checks to ../regression/linking-goto-binaries test …
NlightNFotis Dec 8, 2023
bda5ed3
Add --no-standard-checks to regression/validate-trace-xml-schema pyth…
NlightNFotis Dec 8, 2023
13a6e0b
Add documentation for new options in goto_check_c.h
NlightNFotis Dec 8, 2023
a485f70
Add new flags to CBMC man page
NlightNFotis Dec 12, 2023
9b52a38
Set the default checks status for both defaults on and off
thomasspriggs Dec 12, 2023
1575958
Combine `NEGATIVE` and `POSITIVE` check macros
thomasspriggs Dec 12, 2023
a5a29ad
Use `get_bool_option` to get `unwinding-assertions` option
thomasspriggs Dec 12, 2023
64a7e54
When `--cover` is used switch off unwinding-assertions
thomasspriggs Dec 12, 2023
07ab70e
Add standard checks to goto-analyzer's man page
NlightNFotis Dec 13, 2023
7838ad8
Remove handling of `malloc-may-fail`.
NlightNFotis Dec 13, 2023
3ec5bfd
Don't expect goto-check negative checks for goto-diff manpage.
NlightNFotis Dec 13, 2023
9747f61
Add negative default checks to ignore list of goto-instrument as well
NlightNFotis Dec 13, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Add negative default checks to ignore list of goto-instrument as well
  • Loading branch information
NlightNFotis committed Dec 13, 2023
commit 9747f611973effabb1dcfd0d0baa3e8c4a61a01f
7 changes: 6 additions & 1 deletion scripts/check_help.sh
Original file line number Diff line number Diff line change
Expand Up @@ -83,10 +83,15 @@ for t in \
echo "$undoc" | sed 's/^/\\fB/;s/-/\\-/g;s/$/\\fR/' >> man_page_opts
done
;;
# We also need ignore the negative default checks for goto-instrument given
# that it's not processing them (but still ends up importing them by using
# the macro PARSE_OPTIONS_GOTO_CHECK). The rationale for ignoring them is
# similar to the goto-diff entry below.
goto-instrument)
for undoc in \
-document-claims-html -document-claims-latex -show-claims \
-no-simplify ; do
-no-simplify -no-pointer-check -no-bounds-check -no-undefined-shift-check \
-no-pointer-primitive-check -no-div-by-zero-check -no-signed-overflow-check ; do
echo "$undoc" >> help_string
echo "$undoc" | sed 's/^/\\fB/;s/-/\\-/g;s/$/\\fR/' >> man_page_opts
done
Expand Down