From dfaf8a901a8783a52a57bf3e2de34f80445824ea Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 1 Oct 2024 11:18:32 +0300 Subject: [PATCH 1/2] Add creduce script for both branches dead --- scripts/creduce/branches.sh | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100755 scripts/creduce/branches.sh diff --git a/scripts/creduce/branches.sh b/scripts/creduce/branches.sh new file mode 100755 index 0000000000..d509a19576 --- /dev/null +++ b/scripts/creduce/branches.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +set -e + +gcc -c -Werror=implicit-function-declaration ./bad.c + +GOBLINTDIR="/home/simmo/dev/goblint/sv-comp/goblint" +OPTS="--conf $GOBLINTDIR/conf/svcomp.json --set ana.specification $GOBLINTDIR/../sv-benchmarks/c/properties/unreach-call.prp bad.c --enable pre.enabled" +LOG="goblint.log" + +$GOBLINTDIR/goblint $OPTS -v &> $LOG + +grep -F "Both branches dead" $LOG From 36525a96746c47129b0fff7262aff5ab41fc3e39 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 1 Oct 2024 11:18:46 +0300 Subject: [PATCH 2/2] Add reduced congruence both branches dead test --- .../15-congruence-hardness-unsound-branches.c | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 tests/regression/37-congruence/15-congruence-hardness-unsound-branches.c diff --git a/tests/regression/37-congruence/15-congruence-hardness-unsound-branches.c b/tests/regression/37-congruence/15-congruence-hardness-unsound-branches.c new file mode 100644 index 0000000000..9105e2bf94 --- /dev/null +++ b/tests/regression/37-congruence/15-congruence-hardness-unsound-branches.c @@ -0,0 +1,11 @@ +// PARAM: --enable ana.int.congruence --enable ana.int.interval +// reduced (via creduce and manually) from sv-benchmarks/c/hardness-nfm22/hardness_codestructure_dependencies_file-70.c + +main() { + int a; + unsigned c = 1; + if (a) + c = 4; + if (c + (c + 2)) // NOWARN + a = 1; +}