Skip to content

Commit d9978b4

Browse files
committed
Don't error out when alias analysis fails during loop assigns inference
1 parent 37d57b3 commit d9978b4

File tree

2 files changed

+5
-4
lines changed

2 files changed

+5
-4
lines changed

regression/contracts/loop_assigns-fail/test.desc

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,11 @@
11
CORE
22
main.c
33
--apply-loop-contracts
4-
activate-multi-line-match
5-
Failed to infer variables being modified by the loop at file main.c line \d+ function main\.\nPlease specify an assigns clause\.\nReason:\nAlias analysis returned UNKNOWN!
6-
^EXIT=6$
4+
^EXIT=10$
75
^SIGNAL=0$
6+
^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
7+
^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILURE$
8+
^VERIFICATION FAILED$
89
--
910
--
1011
This test (taken from #6021) shows the need for assigns clauses on loops.

src/goto-instrument/loop_utils.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ void get_assigns_lhs(
5252
const typecast_exprt typed_mod{mod, ptr.pointer.type()};
5353
if(mod.id() == ID_unknown)
5454
{
55-
throw analysis_exceptiont("Alias analysis returned UNKNOWN!");
55+
continue;
5656
}
5757
if(ptr.offset.is_nil())
5858
assigns.insert(dereference_exprt{typed_mod});

0 commit comments

Comments
 (0)