From 5a3f5b4f3824825c4c6fdb2749e26e8beb43cf4d Mon Sep 17 00:00:00 2001 From: septract Date: Thu, 13 Jun 2024 16:50:07 -0700 Subject: [PATCH 1/2] Add check-all.sh script, move out-of-place examples --- .../error-crash/00007-string-transfer-no-io.c | 0 .../{00182.err2.c => 00182.timeout.c} | 0 .../working/{00112.c => 00112.working.c} | 0 src/example-archive/check-all.sh | 43 +++++++++++++++++++ src/example-archive/check.sh | 2 +- .../00005_bit_switch.c | 0 .../00011_dependen_specifications.c | 0 7 files changed, 44 insertions(+), 1 deletion(-) rename src/example-archive/Rust/broken/{ => error-proof}/error-crash/00007-string-transfer-no-io.c (100%) rename src/example-archive/c-testsuite/broken/error-timeout/{00182.err2.c => 00182.timeout.c} (100%) rename src/example-archive/c-testsuite/working/{00112.c => 00112.working.c} (100%) create mode 100644 src/example-archive/check-all.sh rename src/example-archive/java_program_verification_challenges/broken/{error-crash => error-timeout}/00005_bit_switch.c (100%) rename src/example-archive/java_program_verification_challenges/broken/{error-proof => error-timeout}/00011_dependen_specifications.c (100%) diff --git a/src/example-archive/Rust/broken/error-crash/00007-string-transfer-no-io.c b/src/example-archive/Rust/broken/error-proof/error-crash/00007-string-transfer-no-io.c similarity index 100% rename from src/example-archive/Rust/broken/error-crash/00007-string-transfer-no-io.c rename to src/example-archive/Rust/broken/error-proof/error-crash/00007-string-transfer-no-io.c diff --git a/src/example-archive/c-testsuite/broken/error-timeout/00182.err2.c b/src/example-archive/c-testsuite/broken/error-timeout/00182.timeout.c similarity index 100% rename from src/example-archive/c-testsuite/broken/error-timeout/00182.err2.c rename to src/example-archive/c-testsuite/broken/error-timeout/00182.timeout.c diff --git a/src/example-archive/c-testsuite/working/00112.c b/src/example-archive/c-testsuite/working/00112.working.c similarity index 100% rename from src/example-archive/c-testsuite/working/00112.c rename to src/example-archive/c-testsuite/working/00112.working.c diff --git a/src/example-archive/check-all.sh b/src/example-archive/check-all.sh new file mode 100644 index 00000000..4f712ac3 --- /dev/null +++ b/src/example-archive/check-all.sh @@ -0,0 +1,43 @@ +#!/usr/bin/env bash + +if [ -n "$1" ] +then + echo "check-all.sh: using CN=$1 in $PWD" + CN="$1" +else + CN=cn +fi + +subdirs=( + "c-testsuite" + "dafny-tutorial" + "java_program_verification_challenges" + "negative-examples" + "open-sut" + "Rust" + "SAW" + "simple-examples" +) +FAILURE=0 + +for subdir in "${subdirs[@]}"; do + cd "$subdir" || continue + + ../check.sh $CN + + if [ $? != 0 ] + then + FAILURE=1 + fi + + cd .. +done + +if [ $FAILURE -eq 0 ]; +then + printf "\n\033[32mTest suite passes:\033[0m all CN tests in the example archive produced expected return codes\n" + exit 0 +else + printf "\n\033[31mTest suite fails:\033[0m one or more CN tests in the example archive produced an unexpected return code\n" + exit 1 +fi \ No newline at end of file diff --git a/src/example-archive/check.sh b/src/example-archive/check.sh index f4606f57..a246a369 100755 --- a/src/example-archive/check.sh +++ b/src/example-archive/check.sh @@ -2,7 +2,7 @@ if [ -n "$1" ] then - echo "using CN=$1 in $PWD" + echo "check.sh: using CN=$1 in $PWD" CN="$1" else CN=cn diff --git a/src/example-archive/java_program_verification_challenges/broken/error-crash/00005_bit_switch.c b/src/example-archive/java_program_verification_challenges/broken/error-timeout/00005_bit_switch.c similarity index 100% rename from src/example-archive/java_program_verification_challenges/broken/error-crash/00005_bit_switch.c rename to src/example-archive/java_program_verification_challenges/broken/error-timeout/00005_bit_switch.c diff --git a/src/example-archive/java_program_verification_challenges/broken/error-proof/00011_dependen_specifications.c b/src/example-archive/java_program_verification_challenges/broken/error-timeout/00011_dependen_specifications.c similarity index 100% rename from src/example-archive/java_program_verification_challenges/broken/error-proof/00011_dependen_specifications.c rename to src/example-archive/java_program_verification_challenges/broken/error-timeout/00011_dependen_specifications.c From 74f88de4b006688ec0a267f7bfc17677991f372d Mon Sep 17 00:00:00 2001 From: septract Date: Mon, 17 Jun 2024 09:28:31 -0700 Subject: [PATCH 2/2] Set chmod +x, recategorize correctly --- src/example-archive/check-all.sh | 0 .../broken/{error-timeout => error-crash}/00005_bit_switch.c | 0 2 files changed, 0 insertions(+), 0 deletions(-) mode change 100644 => 100755 src/example-archive/check-all.sh rename src/example-archive/java_program_verification_challenges/broken/{error-timeout => error-crash}/00005_bit_switch.c (100%) diff --git a/src/example-archive/check-all.sh b/src/example-archive/check-all.sh old mode 100644 new mode 100755 diff --git a/src/example-archive/java_program_verification_challenges/broken/error-timeout/00005_bit_switch.c b/src/example-archive/java_program_verification_challenges/broken/error-crash/00005_bit_switch.c similarity index 100% rename from src/example-archive/java_program_verification_challenges/broken/error-timeout/00005_bit_switch.c rename to src/example-archive/java_program_verification_challenges/broken/error-crash/00005_bit_switch.c