diff --git a/regression/crangler/loop-invariant-03/main.c b/regression/crangler/loop-invariant-03/main.c new file mode 100644 index 00000000000..a0b723e699f --- /dev/null +++ b/regression/crangler/loop-invariant-03/main.c @@ -0,0 +1,26 @@ +int foo(int *arr, int size) +{ + arr[0] = 0; + arr[size - 1] = 0; + for(int i = 0; i < 2; i++) + { + arr[i] = 0; + } + + int i = 0; + while(i < 2) + { + arr[i] = 0; + i++; + } + + return size < 10 ? 0 : arr[5]; +} + +int main() +{ + int arr[10]; + int retval = foo(arr, 10); + __CPROVER_assert(retval == arr[5], "should succeed"); + return 0; +} diff --git a/regression/crangler/loop-invariant-03/test.desc b/regression/crangler/loop-invariant-03/test.desc new file mode 100644 index 00000000000..1148d96e8a8 --- /dev/null +++ b/regression/crangler/loop-invariant-03/test.desc @@ -0,0 +1,10 @@ +CORE +test.json + +^\s+while\(i \< 2\) \_\_CPROVER\_loop\_invariant +^EXIT=0$ +^SIGNAL=0$ +-- +^\s+for\(int i = 0; i \< 2; i\+\+\) \_\_CPROVER +-- +Annotate loop invariant only to the second loop. diff --git a/regression/crangler/loop-invariant-03/test.json b/regression/crangler/loop-invariant-03/test.json new file mode 100644 index 00000000000..91f004c221f --- /dev/null +++ b/regression/crangler/loop-invariant-03/test.json @@ -0,0 +1,5 @@ +{ + "sources" : ["main.c"], + "functions" : [{"foo": ["loop 2 invariant 1==1"]}], + "output" : "stdout" +} diff --git a/src/crangler/c_wrangler.cpp b/src/crangler/c_wrangler.cpp index a92e610caa9..85db8465a83 100644 --- a/src/crangler/c_wrangler.cpp +++ b/src/crangler/c_wrangler.cpp @@ -213,8 +213,8 @@ void c_wranglert::configure_functions(const jsont &config) function_config.assertions.emplace_back(split[1], rest.str()); } else if( - (split[0] == "for" && split.size() >= 3 && split[2] == "invariant") || - (split[0] == "while" && split.size() >= 3 && split[2] == "invariant")) + (split[0] == "for" || split[0] == "while" || split[0] == "loop") && + split.size() >= 3 && split[2] == "invariant") { std::ostringstream rest; join_strings(rest, split.begin() + 3, split.end(), ' '); @@ -434,7 +434,10 @@ static void mangle_function( { while_count++; const auto &invariant = - loop_invariants["while" + std::to_string(while_count)]; + loop_invariants.count("while" + std::to_string(while_count)) + ? loop_invariants["while" + std::to_string(while_count)] + : loop_invariants + ["loop" + std::to_string(while_count + for_count)]; if(!invariant.empty()) { @@ -449,7 +452,10 @@ static void mangle_function( { for_count++; const auto &invariant = - loop_invariants["for" + std::to_string(for_count)]; + loop_invariants.count("for" + std::to_string(for_count)) + ? loop_invariants["for" + std::to_string(for_count)] + : loop_invariants + ["loop" + std::to_string(while_count + for_count)]; if(!invariant.empty()) {