diff --git a/regression/contracts/invar_assigns_empty/test.desc b/regression/contracts/invar_assigns_empty/test.desc index 69966423ea5..381f619c6c1 100644 --- a/regression/contracts/invar_assigns_empty/test.desc +++ b/regression/contracts/invar_assigns_empty/test.desc @@ -3,8 +3,8 @@ main.c --apply-loop-contracts ^EXIT=0$ ^SIGNAL=0$ -^\[main.1\] .* Check loop invariant before entry: SUCCESS$ -^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts/invar_loop_constant_pass/test_unwind.desc b/regression/contracts/invar_loop_constant_pass/test_unwind.desc new file mode 100644 index 00000000000..30b7613a13b --- /dev/null +++ b/regression/contracts/invar_loop_constant_pass/test_unwind.desc @@ -0,0 +1,14 @@ +CORE +main.c +--apply-loop-contracts --unwind 1 --unwinding-assertions +^EXIT=0$ +^SIGNAL=0$ +^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assigns.\d+\] .* Check that s is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion s == 1: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +This test checks that there is no loop after contract transforamtion. diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 58512048d59..c9032c55707 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -36,6 +36,8 @@ Date: February 2016 #include #include #include +#include +#include #include #include "cfg_info.h" @@ -1016,6 +1018,17 @@ void code_contractst::apply_loop_contract( goto_functions.update(); natural_loops_mutablet updated_loops(goto_function.body); + // We will unwind all transformed loops twice. Store the names of + // to-unwind-loops here and perform the unwinding after transformation done. + // As described in `check_apply_loop_contracts`, loops with loop contracts + // will be transformed to a loop that execute exactly twice: one for base + // case and one for step case. So we unwind them here to avoid users + // incorrectly unwind them only once. + std::string to_unwind = id2string(function_name) + "." + + std::to_string(loop_node.end_target->loop_number) + + ":2"; + loop_names.push_back(to_unwind); + check_apply_loop_contracts( function_name, goto_function, @@ -1459,6 +1472,12 @@ void code_contractst::apply_loop_contracts( "of static/global variables." << messaget::eom; nondet_static(goto_model, to_exclude_from_nondet_init); + + // unwind all transformed loops twice. + unwindsett unwindset{goto_model}; + unwindset.parse_unwindset(loop_names, log.get_message_handler()); + goto_unwindt goto_unwind; + goto_unwind(goto_model, unwindset, goto_unwindt::unwind_strategyt::ASSUME); } void code_contractst::enforce_contracts( diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index 6c5839f1117..2c8f7ddf63d 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -141,6 +141,9 @@ class code_contractst std::unordered_set summarized; + /// Name of loops we are going to unwind. + std::list loop_names; + public: /// Translates a function_pointer_obeys_contract_exprt into an assertion /// ```