handle non-affine conditions in while loops
commitfeaa3b372a3596fb99c65f2463e4d2d4e2dc2d8e
authorSven Verdoolaege <skimo@kotnet.org>
Sun, 1 Jan 2012 22:19:31 +0000 (1 23:19 +0100)
committerSven Verdoolaege <skimo@kotnet.org>
Sun, 3 Jun 2012 11:41:54 +0000 (3 13:41 +0200)
tree66c632bc9aa1aa98893814b196df70fc1a68251f
parent916efcabeab0e190ab3aefd8005fd1d4b51ed6e8
handle non-affine conditions in while loops

We also extend the meaning of an argument to an access expression
to also allow non-single valued arguments.  In these cases, the constraint
on the filter values is assumed to hold for all accessed filter elements.
We use this to make the body of the loop depend on the while condition
evaluating to true for all iterations of the loop up to and including the
current iteration.
The statement that computes the while condition is created in such
a way that it depends on the condition evaluating to true for all
previous iterations.

Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>
include/pet.h
scan.cc
tests/while.c [new file with mode: 0644]
tests/while.scop [new file with mode: 0644]
tests/while_overflow.c [new file with mode: 0644]
tests/while_overflow.scop [new file with mode: 0644]