diff --git a/regression/contracts/invar_check_01/main.c b/regression/contracts/invar_check_01/main.c deleted file mode 100644 index d23252ebd6b..00000000000 --- a/regression/contracts/invar_check_01/main.c +++ /dev/null @@ -1,20 +0,0 @@ -// invar_check_01 - -// This test checks that a basic loop invariant can be proven and used in -// combination with the negation of the loop guard to get a result. - -#include - -int main() -{ - int r; - __CPROVER_assume(r >= 0); - while(r > 0) - __CPROVER_loop_invariant(r >= 0) - { - --r; - } - assert(r == 0); - - return 0; -} diff --git a/regression/contracts/invar_check_01/test.desc b/regression/contracts/invar_check_01/test.desc deleted file mode 100644 index 7dafb10d751..00000000000 --- a/regression/contracts/invar_check_01/test.desc +++ /dev/null @@ -1,11 +0,0 @@ -KNOWNBUG -main.c ---apply-code-contracts -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- --- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/invar_check_02/test.desc b/regression/contracts/invar_check_02/test.desc deleted file mode 100644 index 7dafb10d751..00000000000 --- a/regression/contracts/invar_check_02/test.desc +++ /dev/null @@ -1,11 +0,0 @@ -KNOWNBUG -main.c ---apply-code-contracts -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- --- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/invar_check_03/test.desc b/regression/contracts/invar_check_03/test.desc deleted file mode 100644 index 7dafb10d751..00000000000 --- a/regression/contracts/invar_check_03/test.desc +++ /dev/null @@ -1,11 +0,0 @@ -KNOWNBUG -main.c ---apply-code-contracts -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- --- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/invar_check_04/main.c b/regression/contracts/invar_check_04/main.c deleted file mode 100644 index 68c2fa4ceea..00000000000 --- a/regression/contracts/invar_check_04/main.c +++ /dev/null @@ -1,30 +0,0 @@ -// invar_check_04 - -// This test checks the handling of break by loop invariants. -// This test is expected to fail along the code path where r is even before -// entering the loop. - -#include - -int main() -{ - int r; - __CPROVER_assume(r >= 0); - - while(r>0) - __CPROVER_loop_invariant(r >= 0) - { - --r; - if (r <= 1) - { - break; - } - else - { - --r; - } - } - assert(r == 0); - - return 0; -} diff --git a/regression/contracts/invar_check_04/test.desc b/regression/contracts/invar_check_04/test.desc deleted file mode 100644 index 58ef2893eb5..00000000000 --- a/regression/contracts/invar_check_04/test.desc +++ /dev/null @@ -1,14 +0,0 @@ -KNOWNBUG -main.c ---apply-code-contracts -^EXIT=10$ -^SIGNAL=0$ -^\[main.1\] .* Loop invariant violated before entry: SUCCESS$ -^\[main.2\] .* Loop invariant not preserved: SUCCESS$ -^\[main.assertion.1\] .* assertion r == 0: FAILURE$ -^VERIFICATION FAILED$ --- --- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/invar_check_02/main.c b/regression/contracts/invar_check_break_fail/main.c similarity index 53% rename from regression/contracts/invar_check_02/main.c rename to regression/contracts/invar_check_break_fail/main.c index fee261011ea..938877b2788 100644 --- a/regression/contracts/invar_check_02/main.c +++ b/regression/contracts/invar_check_break_fail/main.c @@ -1,7 +1,3 @@ -// invar_check_02 - -// This test checks that loop invariants adequately handle continues. - #include int main() @@ -11,17 +7,17 @@ int main() while(r > 0) __CPROVER_loop_invariant(r >= 0) - { - --r; - if (r < 5) - { - continue; - } - else { --r; + if(r <= 1) + { + break; + } + else + { + --r; + } } - } assert(r == 0); diff --git a/regression/contracts/invar_check_break_fail/test.desc b/regression/contracts/invar_check_break_fail/test.desc new file mode 100644 index 00000000000..8dcb8ede040 --- /dev/null +++ b/regression/contracts/invar_check_break_fail/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.1\] .* Check loop invariant before entry: SUCCESS$ +^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.1\] .* assertion r == 0: FAILURE$ +^VERIFICATION FAILED$ +-- +This test is expected to fail along the code path where r is an even integer +before entering the loop. +The program is simply incompatible with the desired property in this case -- +there is no loop invariant that can establish the required assertion. diff --git a/regression/contracts/invar_check_break_pass/main.c b/regression/contracts/invar_check_break_pass/main.c new file mode 100644 index 00000000000..c64e2325695 --- /dev/null +++ b/regression/contracts/invar_check_break_pass/main.c @@ -0,0 +1,25 @@ +#include + +int main() +{ + int r; + __CPROVER_assume(r >= 0); + + while(r > 0) + __CPROVER_loop_invariant(r >= 0) + { + --r; + if(r <= 1) + { + break; + } + else + { + --r; + } + } + + assert(r == 0 || r == 1); + + return 0; +} diff --git a/regression/contracts/invar_check_break_pass/test.desc b/regression/contracts/invar_check_break_pass/test.desc new file mode 100644 index 00000000000..ea11f37bf07 --- /dev/null +++ b/regression/contracts/invar_check_break_pass/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.1\] .* Check loop invariant before entry: SUCCESS$ +^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.1\] .* assertion r == 0 || r == 1: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +This test checks that conditionals and `break` are correctly handled. diff --git a/regression/contracts/invar_check_continue/main.c b/regression/contracts/invar_check_continue/main.c new file mode 100644 index 00000000000..22440cf5f15 --- /dev/null +++ b/regression/contracts/invar_check_continue/main.c @@ -0,0 +1,25 @@ +#include + +int main() +{ + int r; + __CPROVER_assume(r >= 0); + + while(r > 0) + __CPROVER_loop_invariant(r >= 0) + { + --r; + if(r < 5) + { + continue; + } + else + { + --r; + } + } + + assert(r == 0); + + return 0; +} diff --git a/regression/contracts/invar_check_continue/test.desc b/regression/contracts/invar_check_continue/test.desc new file mode 100644 index 00000000000..654d25185aa --- /dev/null +++ b/regression/contracts/invar_check_continue/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.1\] .* Check loop invariant before entry: SUCCESS$ +^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.1\] .* assertion r == 0: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +This test checks that conditionals and `continue` are correctly handled. diff --git a/regression/contracts/invar_check_03/main.c b/regression/contracts/invar_check_large/main.c similarity index 71% rename from regression/contracts/invar_check_03/main.c rename to regression/contracts/invar_check_large/main.c index 253e5a951d6..2dd6507c952 100644 --- a/regression/contracts/invar_check_03/main.c +++ b/regression/contracts/invar_check_large/main.c @@ -1,10 +1,3 @@ -// invar_check_03 - -// This test checks the use of loop invariants on a larger problem --- in this -// case, the partition portion of quicksort, applied to a fixed-length array. -// This serves as a stop-gap test until issues to do with quantifiers and -// side-effects in loop invariants are fixed. - #include void swap(int *a, int *b) @@ -15,13 +8,13 @@ void swap(int *a, int *b) } int main() -{ +{ int arr0, arr1, arr2, arr3, arr4; arr0 = 1; arr1 = 2; arr2 = 0; arr3 = 4; - arr4 = 3; + arr4 = 3; int *arr[5] = {&arr0, &arr1, &arr2, &arr3, &arr4}; int pivot = 2; @@ -30,6 +23,8 @@ int main() int r = 1; while(h > l) __CPROVER_loop_invariant( + // Turn off `clang-format` because it breaks the `==>` operator. + /* clang-format off */ h >= l && 0 <= l && l < 5 && 0 <= h && h < 5 && @@ -49,26 +44,35 @@ int main() (2 > h ==> arr2 >= pivot) && (3 > h ==> arr3 >= pivot) && (4 > h ==> arr4 >= pivot) + /* clang-format on */ ) - { - if(*(arr[h]) <= pivot && *(arr[l]) >= pivot) { - swap(arr[h], arr[l]); - if (r == h) { - r = l; - h--; + { + if(*(arr[h]) <= pivot && *(arr[l]) >= pivot) + { + swap(arr[h], arr[l]); + if(r == h) + { + r = l; + h--; + } + else if(r == l) + { + r = h; + l++; + } } - else if(r == l) { - r = h; + else if(*(arr[h]) <= pivot) + { l++; } + else + { + h--; + } } - else if(*(arr[h]) <= pivot) { - l++; - } - else { - h--; - } - } + + // Turn off `clang-format` because it breaks the `==>` operator. + /* clang-format off */ assert(0 <= r && r < 5); assert(*(arr[r]) == pivot); assert(0 < r ==> arr0 <= pivot); @@ -81,5 +85,7 @@ int main() assert(2 > r ==> arr2 >= pivot); assert(3 > r ==> arr3 >= pivot); assert(4 > r ==> arr4 >= pivot); + /* clang-format on */ + return r; } diff --git a/regression/contracts/invar_check_large/test.desc b/regression/contracts/invar_check_large/test.desc new file mode 100644 index 00000000000..f5c18f62587 --- /dev/null +++ b/regression/contracts/invar_check_large/test.desc @@ -0,0 +1,25 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.1\] .* Check loop invariant before entry: SUCCESS$ +^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.1\] .* assertion 0 <= r && r < 5: SUCCESS$ +^\[main.assertion.2\] .* assertion \*\(arr\[r\]\) == pivot: SUCCESS$ +^\[main.assertion.3\] .* assertion 0 < r ==> arr0 <= pivot: SUCCESS$ +^\[main.assertion.4\] .* assertion 1 < r ==> arr1 <= pivot: SUCCESS$ +^\[main.assertion.5\] .* assertion 2 < r ==> arr2 <= pivot: SUCCESS$ +^\[main.assertion.6\] .* assertion 3 < r ==> arr3 <= pivot: SUCCESS$ +^\[main.assertion.7\] .* assertion 4 < r ==> arr4 <= pivot: SUCCESS$ +^\[main.assertion.8\] .* assertion 0 > r ==> arr0 >= pivot: SUCCESS$ +^\[main.assertion.9\] .* assertion 1 > r ==> arr1 >= pivot: SUCCESS$ +^\[main.assertion.10\] .* assertion 2 > r ==> arr2 >= pivot: SUCCESS$ +^\[main.assertion.11\] .* assertion 3 > r ==> arr3 >= pivot: SUCCESS$ +^\[main.assertion.12\] .* assertion 4 > r ==> arr4 >= pivot: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +This test checks the invariant contracts on a larger problem --- in this case, +the partition function of quicksort, applied to a fixed-length array. +This serves as a stop-gap test until issues to do with quantifiers and +side-effects in loop invariants are fixed. diff --git a/regression/contracts/invar_check_multiple_loops/main.c b/regression/contracts/invar_check_multiple_loops/main.c new file mode 100644 index 00000000000..b30322b8258 --- /dev/null +++ b/regression/contracts/invar_check_multiple_loops/main.c @@ -0,0 +1,23 @@ +#include + +int main() +{ + int r, n, x, y; + __CPROVER_assume(n > 0 && x == y); + + for(r = 0; r < n; ++r) + __CPROVER_loop_invariant(0 <= r && r <= n && x == y + r) + { + x++; + } + while(r > 0) + __CPROVER_loop_invariant(r >= 0 && x == y + n + (n - r)) + { + y--; + r--; + } + + assert(x == y + 2 * n); + + return 0; +} diff --git a/regression/contracts/invar_check_multiple_loops/test.desc b/regression/contracts/invar_check_multiple_loops/test.desc new file mode 100644 index 00000000000..0b2578bc594 --- /dev/null +++ b/regression/contracts/invar_check_multiple_loops/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.1\] .* Check loop invariant before entry: SUCCESS$ +^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.3\] .* Check loop invariant before entry: SUCCESS$ +^\[main.4\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.1\] .* assertion x == y \+ 2 \* n: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +This test checks that multiple loops and `for` loops are correctly handled. diff --git a/regression/contracts/invar_check_nested_loops/main.c b/regression/contracts/invar_check_nested_loops/main.c new file mode 100644 index 00000000000..a83aa6a26f6 --- /dev/null +++ b/regression/contracts/invar_check_nested_loops/main.c @@ -0,0 +1,27 @@ +#include + +int main() +{ + int n, s = 0; + __CPROVER_assume(n >= 0); + + for(int i = 0; i < n; ++i) + __CPROVER_loop_invariant(i <= n && s == i) + { + int a, b; + __CPROVER_assume(b >= 0 && a == b); + + while(a > 0) + __CPROVER_loop_invariant(a >= 0 && s == i + (b - a)) + { + s++; + a--; + } + + s -= (b - 1); + } + + assert(s == n); + + return 0; +} diff --git a/regression/contracts/invar_check_nested_loops/test.desc b/regression/contracts/invar_check_nested_loops/test.desc new file mode 100644 index 00000000000..e1f59d8e91d --- /dev/null +++ b/regression/contracts/invar_check_nested_loops/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.1\] .* Check loop invariant before entry: SUCCESS$ +^\[main.4\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.2\] .* Check loop invariant before entry: SUCCESS$ +^\[main.3\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.1\] .* assertion s == n: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +This test checks that nested loops, `for` loops, +and loop-local declarations of the index variable are correctly handled. diff --git a/regression/contracts/invar_check_sufficiency/main.c b/regression/contracts/invar_check_sufficiency/main.c new file mode 100644 index 00000000000..b650ef25181 --- /dev/null +++ b/regression/contracts/invar_check_sufficiency/main.c @@ -0,0 +1,17 @@ +#include + +int main() +{ + int r; + __CPROVER_assume(r >= 0); + + while(r > 0) + __CPROVER_loop_invariant(r >= 0) + { + --r; + } + + assert(r == 0); + + return 0; +} diff --git a/regression/contracts/invar_check_sufficiency/test.desc b/regression/contracts/invar_check_sufficiency/test.desc new file mode 100644 index 00000000000..a76c7b312b4 --- /dev/null +++ b/regression/contracts/invar_check_sufficiency/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.1\] .* Check loop invariant before entry: SUCCESS$ +^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.1\] .* assertion r == 0: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +This test checks that a loop invariant can be proven to be inductive, +and is used in conjunction with the negation of the loop guard +to establish the postcondition. diff --git a/regression/contracts/invar_loop_constant/main.c b/regression/contracts/invar_loop_constant/main.c deleted file mode 100644 index 34eb0575d53..00000000000 --- a/regression/contracts/invar_loop_constant/main.c +++ /dev/null @@ -1,25 +0,0 @@ -// invar_loop_constant - -// This test checks to see whether loop invariant checking discards sufficiently -// little information to be aware after the loop that s is necessarily 1. -// This test currently fails due to excessive havocking in checking loop -// invariants, but is not an obstacle to soundness of contract checking. - -#include - -int main() -{ - int r; - int s = 1; - __CPROVER_assume(r >= 0); - while(r > 0) - __CPROVER_loop_invariant(r >= 0) - { - s = 1; - r--; - } - assert(r == 0); - assert(s == 1); - - return 0; -} diff --git a/regression/contracts/invar_loop_constant/test.desc b/regression/contracts/invar_loop_constant/test.desc deleted file mode 100644 index a27604a79fd..00000000000 --- a/regression/contracts/invar_loop_constant/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -KNOWNBUG -main.c ---check-code-contracts -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- --- -Loop invariant checking throws away more information than needed. diff --git a/regression/contracts/invar_loop_constant_fail/main.c b/regression/contracts/invar_loop_constant_fail/main.c new file mode 100644 index 00000000000..c2085486cb6 --- /dev/null +++ b/regression/contracts/invar_loop_constant_fail/main.c @@ -0,0 +1,18 @@ +#include + +int main() +{ + int r; + int s = 1; + __CPROVER_assume(r >= 0); + while(r > 0) + __CPROVER_loop_invariant(r >= 0) + { + s = 1; + r--; + } + assert(r == 0); + assert(s == 1); + + return 0; +} diff --git a/regression/contracts/invar_loop_constant_fail/test.desc b/regression/contracts/invar_loop_constant_fail/test.desc new file mode 100644 index 00000000000..1411c8a199b --- /dev/null +++ b/regression/contracts/invar_loop_constant_fail/test.desc @@ -0,0 +1,18 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.1\] .* Check loop invariant before entry: SUCCESS$ +^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.1\] .* assertion r == 0: SUCCESS$ +^\[main.assertion.2\] .* assertion s == 1: FAILURE$ +^VERIFICATION FAILED$ +-- +This test is expected to fail because it modifies a variable within a loop, +but attempts to check that it is "effectively constant" without asserting so +within the loop invariant. +The current implementation of `check_apply_invariant` correctly havocs all +variables that are modified within the loop. +The fact that a variable is "effectively constant" within a loop must be +established using an appropriate clause in the invariant. diff --git a/regression/contracts/invar_loop_constant_no_modify/main.c b/regression/contracts/invar_loop_constant_no_modify/main.c new file mode 100644 index 00000000000..b57995c0987 --- /dev/null +++ b/regression/contracts/invar_loop_constant_no_modify/main.c @@ -0,0 +1,17 @@ +#include + +int main() +{ + int r; + int s = 1; + __CPROVER_assume(r >= 0); + while(r > 0) + __CPROVER_loop_invariant(r >= 0) + { + r--; + } + assert(r == 0); + assert(s == 1); + + return 0; +} diff --git a/regression/contracts/invar_loop_constant_no_modify/test.desc b/regression/contracts/invar_loop_constant_no_modify/test.desc new file mode 100644 index 00000000000..fa38c4d19e5 --- /dev/null +++ b/regression/contracts/invar_loop_constant_no_modify/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.1\] .* Check loop invariant before entry: SUCCESS$ +^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.1\] .* assertion r == 0: SUCCESS$ +^\[main.assertion.2\] .* assertion s == 1: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +This test checks that variables that are not modified within the loop +are not unnecessarily havoced by `check_apply_invariant`. diff --git a/regression/contracts/invar_loop_constant_pass/main.c b/regression/contracts/invar_loop_constant_pass/main.c new file mode 100644 index 00000000000..8e85f3cb140 --- /dev/null +++ b/regression/contracts/invar_loop_constant_pass/main.c @@ -0,0 +1,17 @@ +#include + +int main() +{ + int r, s = 1; + __CPROVER_assume(r >= 0); + while(r > 0) + __CPROVER_loop_invariant(r >= 0 && s == 1) + { + s = 1; + r--; + } + assert(r == 0); + assert(s == 1); + + return 0; +} diff --git a/regression/contracts/invar_loop_constant_pass/test.desc b/regression/contracts/invar_loop_constant_pass/test.desc new file mode 100644 index 00000000000..b272e4d3ecd --- /dev/null +++ b/regression/contracts/invar_loop_constant_pass/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.1\] .* Check loop invariant before entry: SUCCESS$ +^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.1\] .* assertion r == 0: SUCCESS$ +^\[main.assertion.2\] .* assertion s == 1: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +This test checks that the invariant is correctly used to satisfy +all assertions that follow a loop. diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 7b1fac1bcef..22e551dc5e2 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -69,15 +69,12 @@ static void check_apply_invariants( PRECONDITION(!loop.empty()); // find the last back edge - goto_programt::targett loop_end=loop_head; - for(loopt::const_iterator - it=loop.begin(); - it!=loop.end(); - ++it) - if((*it)->is_goto() && - (*it)->get_target()==loop_head && - (*it)->location_number>loop_end->location_number) - loop_end=*it; + goto_programt::targett loop_end = loop_head; + for(const auto &t : loop) + if( + t->is_goto() && t->get_target() == loop_head && + t->location_number > loop_end->location_number) + loop_end = t; // see whether we have an invariant exprt invariant = static_cast( @@ -107,7 +104,7 @@ static void check_apply_invariants( { goto_programt::targett a = havoc_code.add( goto_programt::make_assertion(invariant, loop_head->source_location)); - a->source_location.set_comment("Loop invariant violated before entry"); + a->source_location.set_comment("Check loop invariant before entry"); } // havoc variables being written to @@ -125,15 +122,15 @@ static void check_apply_invariants( side_effect_expr_nondett(bool_typet(), loop_head->source_location))); } - // Now havoc at the loop head. Use insert_swap to - // preserve jumps to loop head. + // Now havoc at the loop head. + // Use insert_before_swap to preserve jumps to loop head. goto_function.body.insert_before_swap(loop_head, havoc_code); // assert the invariant at the end of the loop body { goto_programt::instructiont a = goto_programt::make_assertion(invariant, loop_end->source_location); - a.source_location.set_comment("Loop invariant not preserved"); + a.source_location.set_comment("Check that loop invariant is preserved"); goto_function.body.insert_before_swap(loop_end, a); ++loop_end; } @@ -158,7 +155,7 @@ bool code_contractst::has_contract(const irep_idt fun_name) type.find(ID_C_spec_ensures).is_not_nil(); } -bool code_contractst::apply_contract( +bool code_contractst::apply_function_contract( goto_programt &goto_program, goto_programt::targett target) { @@ -299,24 +296,16 @@ bool code_contractst::apply_contract( return false; } -void code_contractst::code_contracts( +void code_contractst::apply_loop_contract( goto_functionst::goto_functiont &goto_function) { local_may_aliast local_may_alias(goto_function); natural_loops_mutablet natural_loops(goto_function.body); // iterate over the (natural) loops in the function - for(natural_loops_mutablet::loop_mapt::const_iterator l_it = - natural_loops.loop_map.begin(); - l_it != natural_loops.loop_map.end(); - l_it++) + for(const auto &loop : natural_loops.loop_map) check_apply_invariants( - goto_function, local_may_alias, l_it->first, l_it->second); - - // look at all function calls - Forall_goto_program_instructions(ins, goto_function.body) - if(ins->is_function_call()) - apply_contract(goto_function.body, ins); + goto_function, local_may_alias, loop.first, loop.second); } const symbolt &code_contractst::new_tmp_symbol( @@ -910,7 +899,7 @@ bool code_contractst::replace_calls( if(found == funs_to_replace.end()) continue; - fail |= apply_contract(goto_function.second.body, ins); + fail |= apply_function_contract(goto_function.second.body, ins); } } } @@ -944,6 +933,8 @@ bool code_contractst::enforce_contracts() { if(has_contract(goto_function.first)) funs_to_enforce.insert(id2string(goto_function.first)); + else + apply_loop_contract(goto_function.second); } return enforce_contracts(funs_to_enforce); } @@ -954,7 +945,8 @@ bool code_contractst::enforce_contracts( bool fail = false; for(const auto &fun : funs_to_enforce) { - if(!has_contract(fun)) + auto goto_function = goto_functions.function_map.find(fun); + if(goto_function == goto_functions.function_map.end()) { fail = true; log.error() << "Could not find function '" << fun @@ -962,9 +954,18 @@ bool code_contractst::enforce_contracts( << messaget::eom; continue; } + apply_loop_contract(goto_function->second); + + if(!has_contract(fun)) + { + fail = true; + log.error() << "Could not find any contracts within function '" << fun + << "'; nothing to enforce." << messaget::eom; + continue; + } if(!fail) - fail |= enforce_contract(fun); + fail = enforce_contract(fun); } return fail; } diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h index 0c696de4437..74c084b2e0e 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/code_contracts.h @@ -133,13 +133,14 @@ class code_contractst goto_programt &created_decls, std::vector &created_references); - void code_contracts(goto_functionst::goto_functiont &goto_function); + void apply_loop_contract(goto_functionst::goto_functiont &goto_function); /// \brief Does the named function have a contract? bool has_contract(const irep_idt); - bool - apply_contract(goto_programt &goto_program, goto_programt::targett target); + bool apply_function_contract( + goto_programt &goto_program, + goto_programt::targett target); void add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest);