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

Show file tree
Hide file tree
Changes from all commits
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
3 changes: 2 additions & 1 deletion regression/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl")
macro(add_test_pl_profile name cmdline flag profile)
add_test(
NAME "${name}-${profile}"
COMMAND ${test_pl_path} -e -p -c ${cmdline} ${flag} ${ARGN}
COMMAND ${test_pl_path} -e -p -c "${cmdline}" ${flag} ${ARGN}
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
)
set_tests_properties("${name}-${profile}" PROPERTIES
Expand Down Expand Up @@ -31,6 +31,7 @@ add_subdirectory(goto-instrument)
add_subdirectory(cpp)
add_subdirectory(cbmc-concurrency)
add_subdirectory(cbmc-cover)
add_subdirectory(cbmc-incr-oneloop)
add_subdirectory(goto-instrument-typedef)
add_subdirectory(smt2_solver)
add_subdirectory(smt2_strings)
Expand Down
1 change: 1 addition & 0 deletions regression/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ DIRS = cbmc \
cpp \
cbmc-concurrency \
cbmc-cover \
cbmc-incr-oneloop \
goto-instrument-typedef \
smt2_solver \
smt2_strings \
Expand Down
3 changes: 3 additions & 0 deletions regression/cbmc-incr-oneloop/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
add_test_pl_tests(
"perl -e 'alarm shift @ARGV; exec @ARGV' 8 $<TARGET_FILE:cbmc> --slice-formula"
)
4 changes: 2 additions & 2 deletions regression/cbmc-incr-oneloop/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
default: tests.log

test:
@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --slice-formula"
@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 8 ../../../src/cbmc/cbmc --slice-formula"
Copy link
Collaborator

Choose a reason for hiding this comment

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

Why is there a perl -e wrapper for those tests?

Copy link
Member Author

Choose a reason for hiding this comment

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

for the timeout

Copy link
Collaborator

Choose a reason for hiding this comment

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

I think a comment would be nice to have.


tests.log: ../test.pl
@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --slice-formula"
@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 8 ../../../src/cbmc/cbmc --slice-formula"

show:
@for dir in *; do \
Expand Down
Loading