Skip to content

Incremental unwinding of one specified loop #4361

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.

Sign up for GitHub

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

Closed
wants to merge 16 commits into from
Closed

Incremental unwinding of one specified loop #4361

Changes from 1 commit
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
54d581b
Allow disabling optimized assertion conversion
peterschrammel Feb 9, 2019
452b524
Hidden field is used for hiding in trace
peterschrammel Feb 9, 2019
1fb7d2d
Allow symex to temporarily ignore assertions
peterschrammel Feb 3, 2019
73fb826
Allow symex_target_equationt to separately convert assertions
peterschrammel Feb 3, 2019
41d3864
Use only remaining properties in property decider
peterschrammel Feb 9, 2019
7fbc6b0
Add callback to decide on interrupting goto-symex
peterschrammel Feb 9, 2019
2a7b16c
Add symex BMC incremental one loop
peterschrammel Feb 9, 2019
cef212c
Add single-loop incremental symex checker
peterschrammel Feb 2, 2019
4e894a4
Add options for incremental one-loop BMC
peterschrammel Feb 3, 2019
d7581bd
Add --incremental-loop to CBMC
peterschrammel Feb 3, 2019
30ca986
Fix quoting in test command
peterschrammel Feb 9, 2019
aa1389b
Make sure output buffers are flushed before writing exit code
peterschrammel Mar 10, 2019
657a899
Clean up cbmc-incr-oneloop tests
peterschrammel Feb 9, 2019
cc60ab3
Set induction tests to FUTURE
peterschrammel Feb 10, 2019
f1af977
Clang-format cbmc-incr-oneloop tests
peterschrammel Feb 10, 2019
20613e8
Ignore properties before unwind min
peterschrammel Feb 10, 2019
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
13 changes: 12 additions & 1 deletion src/goto-checker/bmc_util.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -188,7 +188,10 @@ void run_property_decider(
"(unwind):" \
"(unwindset):" \
"(graphml-witness):" \
"(unwindset):"
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I was confused at first - maybe we should have a separate commit that cleans up this duplicate (unwindset):?

"(incremental-loop):" \
"(unwind-min):" \
"(unwind-max):" \
"(ignore-properties-before-unwind-min)"

#define HELP_BMC \
" --paths [strategy] explore paths one at a time\n" \
Expand All @@ -201,6 +204,14 @@ void run_property_decider(
" --unwind nr unwind nr times\n" \
" --unwindset L:B,... unwind loop L with a bound of B\n" \
" (use --show-loops to get the loop IDs)\n" \
" --incremental-loop L check properties after each unwinding\n" \
" of loop L\n" \
" (use --show-loops to get the loop IDs)\n" \
" --unwind-min nr start incremental-loop after nr unwindings\n" \
" --unwind-max nr stop incremental-loop after nr unwindings\n" \
" --ignore-properties-before-unwind-min\n" \
" do not check properties before unwind-min\n" \
" when using incremental-loop\n" \
" --show-vcc show the verification conditions\n" \
" --slice-formula remove assignments unrelated to property\n" \
" --unwinding-assertions generate unwinding assertions (cannot be\n" \
Expand Down