From 61a4071e501eb02870811e90f3b51370a645cc3b Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 6 Aug 2024 16:21:46 +0200 Subject: [PATCH] Add regression test --- tests/regression/46-apron2/98-issue-1511b.c | 32 +++++++++++++++++ tests/regression/46-apron2/98-issue-1511b.t | 40 +++++++++++++++++++++ 2 files changed, 72 insertions(+) create mode 100644 tests/regression/46-apron2/98-issue-1511b.c create mode 100644 tests/regression/46-apron2/98-issue-1511b.t diff --git a/tests/regression/46-apron2/98-issue-1511b.c b/tests/regression/46-apron2/98-issue-1511b.c new file mode 100644 index 0000000000..6ba233b61b --- /dev/null +++ b/tests/regression/46-apron2/98-issue-1511b.c @@ -0,0 +1,32 @@ +#include +int d, j, k; + +pthread_mutex_t f; + +void nothing() {}; +void nothing2() {}; + +int top() { + int top2; + return top2; +} + +void main() { + d = top(); + if (d) { + k = 1; + pthread_t tid; + pthread_create(&tid, 0, ¬hing, NULL); + pthread_mutex_lock(&f); + j = 0; // To ensure something is published + pthread_mutex_unlock(&f); + pthread_mutex_lock(&f); + + pthread_t tid2; + pthread_create(&tid2, 0, ¬hing2, NULL); + float f = 8.0f; + } else { + pthread_t tid2; + pthread_create(&tid2, 0, ¬hing2, NULL); + } +} diff --git a/tests/regression/46-apron2/98-issue-1511b.t b/tests/regression/46-apron2/98-issue-1511b.t new file mode 100644 index 0000000000..8add2f3d1c --- /dev/null +++ b/tests/regression/46-apron2/98-issue-1511b.t @@ -0,0 +1,40 @@ + $ goblint --disable warn.unsound --disable warn.imprecise --disable sem.unknown_function.invalidate.globals --enable warn.deterministic --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid --enable witness.yaml.enabled --disable witness.invariant.other --disable witness.invariant.loop-head 98-issue-1511b.c --set witness.yaml.path 98-issue-1511b.yml + [Info][Witness] witness generation summary: + total generation entries: 27 + + $ goblint --disable warn.unsound --disable warn.imprecise --disable sem.unknown_function.invalidate.globals --enable warn.deterministic --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 98-issue-1511b.yml 98-issue-1511b.c + [Info][Witness] witness validation summary: + confirmed: 52 + unconfirmed: 0 + refuted: 0 + error: 0 + unchecked: 0 + unsupported: 0 + disabled: 0 + total validation entries: 52 + [Success][Witness] invariant confirmed: (1LL + (long long )j) - (long long )k >= 0LL (98-issue-1511b.c:21:5) + [Success][Witness] invariant confirmed: (1LL - (long long )j) - (long long )k >= 0LL (98-issue-1511b.c:21:5) + [Success][Witness] invariant confirmed: (2147483646LL + (long long )j) + (long long )k >= 0LL (98-issue-1511b.c:21:5) + [Success][Witness] invariant confirmed: (2147483646LL - (long long )d) + (long long )k >= 0LL (98-issue-1511b.c:21:5) + [Success][Witness] invariant confirmed: (2147483646LL - (long long )j) + (long long )k >= 0LL (98-issue-1511b.c:21:5) + [Success][Witness] invariant confirmed: (2147483647LL + (long long )d) + (long long )k >= 0LL (98-issue-1511b.c:21:5) + [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) + (long long )j >= 0LL (98-issue-1511b.c:21:5) + [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) - (long long )j >= 0LL (98-issue-1511b.c:21:5) + [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) + (long long )j >= 0LL (98-issue-1511b.c:21:5) + [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) - (long long )j >= 0LL (98-issue-1511b.c:21:5) + [Success][Witness] invariant confirmed: (2147483648LL - (long long )d) - (long long )k >= 0LL (98-issue-1511b.c:21:5) + [Success][Witness] invariant confirmed: (2147483649LL + (long long )d) - (long long )k >= 0LL (98-issue-1511b.c:21:5) + [Success][Witness] invariant confirmed: j == 0 (98-issue-1511b.c:21:5) + [Success][Witness] invariant confirmed: (1LL + (long long )j) - (long long )k >= 0LL (98-issue-1511b.c:26:5) + [Success][Witness] invariant confirmed: (1LL - (long long )j) - (long long )k >= 0LL (98-issue-1511b.c:26:5) + [Success][Witness] invariant confirmed: (2147483646LL + (long long )j) + (long long )k >= 0LL (98-issue-1511b.c:26:5) + [Success][Witness] invariant confirmed: (2147483646LL - (long long )d) + (long long )k >= 0LL (98-issue-1511b.c:26:5) + [Success][Witness] invariant confirmed: (2147483646LL - (long long )j) + (long long )k >= 0LL (98-issue-1511b.c:26:5) + [Success][Witness] invariant confirmed: (2147483647LL + (long long )d) + (long long )k >= 0LL (98-issue-1511b.c:26:5) + [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) + (long long )j >= 0LL (98-issue-1511b.c:26:5) + [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) - (long long )j >= 0LL (98-issue-1511b.c:26:5) + [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) + (long long )j >= 0LL (98-issue-1511b.c:26:5) + [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) - (long long )j >= 0LL (98-issue-1511b.c:26:5) + [Success][Witness] invariant confirmed: (2147483648LL - (long long )d) - (long long )k >= 0LL (98-issue-1511b.c:26:5) + [Success][Witness] invariant confirmed: (2147483649LL + (long long )d) - (long long )k >= 0LL (98-issue-1511b.c:26:5) + [Success][Witness] invariant confirmed: j == 0 (98-issue-1511b.c:26:5)