From 54595bd64af99d1c14a436b1fa768a3e99e522a7 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Fri, 29 Nov 2024 16:01:43 +0100 Subject: [PATCH] new ways to spot unreachable code --- tests/regression/77-lin2vareq/35-refinement.c | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/tests/regression/77-lin2vareq/35-refinement.c b/tests/regression/77-lin2vareq/35-refinement.c index 1d791d6e4f..df2bf14c5b 100644 --- a/tests/regression/77-lin2vareq/35-refinement.c +++ b/tests/regression/77-lin2vareq/35-refinement.c @@ -10,7 +10,7 @@ void main() { int d = 13*a+11; int e = a; - if (b < 5){ // a < 1 + if (b < 5){ // a > -1 __goblint_check(1 == 1); //SUCCESS __goblint_check(a > -1); //SUCCESS @@ -35,6 +35,11 @@ void main() { __goblint_check(c > 0); //SUCCESS __goblint_check(d < 24); //SUCCESS + if (b < 3) { + __goblint_check(0); //NOWARN (unreachable) + b = 1701; + } + // in theory, if we knew about a being constant, we could infer the following: __goblint_check(b == 3); //UNKNOWN __goblint_check(c == 5); //UNKNOWN