Skip to content

Commit d82727b

Browse files
committed
Make variables unsigned in 89-apron3/{01,02}
Avoids accidental boundedness from assume_none.
1 parent 1f63c72 commit d82727b

File tree

2 files changed

+10
-10
lines changed

2 files changed

+10
-10
lines changed

tests/regression/89-apron3/01-halbwachs-phd-sec5.6.2.c

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
1-
// SKIP TERM PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set sem.int.signed_overflow assume_none --set ana.activated[+] termination
1+
// SKIP TERM PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set ana.activated[+] termination
22
// fully works with --set ana.widen.delay.local 6
33
// Somehow we prove termination even without and don't have good bounds on termination counter.
44
// From Nicolas Halbwachs' PhD thesis, section 5.6.2.
55
#include <goblint.h>
66

77
int main() {
8-
int i = 0;
9-
int j = 0;
8+
unsigned int i = 0;
9+
unsigned int j = 0;
1010
while (i <= 10) {
1111
__goblint_check(j >= 0);
1212
__goblint_check(i - 2 * j >= 0);
@@ -22,7 +22,7 @@ int main() {
2222
}
2323

2424
__goblint_check(j >= 0);
25-
__goblint_check(i - 2 * j >= 0); // requires sem.int.signed_overflow assume_none without narrowing because no upper bound on j
25+
__goblint_check(i - 2 * j >= 0);
2626
__goblint_check(11 <= i);
2727
__goblint_check(i <= 14); // TODO: needs one narrowing iteration
2828
__goblint_check(i + 2 * j <= 24); // TODO: needs one narrowing iteration

tests/regression/89-apron3/02-halbwachs-phd-sec8.3.c

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
1-
// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set sem.int.signed_overflow assume_none
1+
// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra
22
// fully works with --set ana.widen.delay.local 6
33
// From Nicolas Halbwachs' PhD thesis, section 8.3.
44
// Same as 01-halbwachs-phd-sec5.6.2 annotated with an explicit termination counter.
55
#include <goblint.h>
66

77
int main() {
8-
int i = 0;
9-
int j = 0;
10-
int k = 0; // explicit termination counter
8+
unsigned int i = 0;
9+
unsigned int j = 0;
10+
unsigned int k = 0; // explicit termination counter
1111
while (k++, i <= 10) {
1212
__goblint_check(j >= 0);
1313
__goblint_check(i + 2 * j + 4 == 4 * k);
@@ -31,10 +31,10 @@ int main() {
3131
}
3232

3333
__goblint_check(j >= 0);
34-
__goblint_check(i + 2 * j + 4 == 4 * k); // requires sem.int.signed_overflow assume_none without narrowing because no upper bound on j
34+
__goblint_check(i + 2 * j + 4 == 4 * k); // TODO: needs one narrowing iteration?
3535
__goblint_check(11 <= i);
3636
__goblint_check(i <= 14); // TODO: needs one narrowing iteration?
37-
__goblint_check(2 * k <= i + 2);
37+
__goblint_check(2 * k <= i + 2); // TODO: needs one narrowing iteration?
3838

3939
// if i and j are projected out:
4040
__goblint_check(4 <= k);

0 commit comments

Comments
 (0)