From a36de69a2ca12f01e0976d36c781ed6260b33124 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 15 Nov 2022 14:15:18 +0000 Subject: [PATCH 1/3] Ensure all readme files are named README.md This is to make them easier to spot when there might be a large number of files or sub-directories in a particular directory. --- .../lambda_examples/{readme.md => README.md} | 0 regression/{readme.md => README.md} | 0 .../cbmc-incr-smt2/bitvector-flag-tests/{readme.md => README.md} | 0 regression/goto-cc-cbmc-shared-options/{readme.md => README.md} | 0 regression/symtab2gb-cbmc/{readme.md => README.md} | 0 regression/symtab2gb/{readme.md => README.md} | 0 scripts/bash-autocomplete/{Readme.md => README.md} | 0 7 files changed, 0 insertions(+), 0 deletions(-) rename jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/lambda_examples/{readme.md => README.md} (100%) rename regression/{readme.md => README.md} (100%) rename regression/cbmc-incr-smt2/bitvector-flag-tests/{readme.md => README.md} (100%) rename regression/goto-cc-cbmc-shared-options/{readme.md => README.md} (100%) rename regression/symtab2gb-cbmc/{readme.md => README.md} (100%) rename regression/symtab2gb/{readme.md => README.md} (100%) rename scripts/bash-autocomplete/{Readme.md => README.md} (100%) diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/lambda_examples/readme.md b/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/lambda_examples/README.md similarity index 100% rename from jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/lambda_examples/readme.md rename to jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/lambda_examples/README.md diff --git a/regression/readme.md b/regression/README.md similarity index 100% rename from regression/readme.md rename to regression/README.md diff --git a/regression/cbmc-incr-smt2/bitvector-flag-tests/readme.md b/regression/cbmc-incr-smt2/bitvector-flag-tests/README.md similarity index 100% rename from regression/cbmc-incr-smt2/bitvector-flag-tests/readme.md rename to regression/cbmc-incr-smt2/bitvector-flag-tests/README.md diff --git a/regression/goto-cc-cbmc-shared-options/readme.md b/regression/goto-cc-cbmc-shared-options/README.md similarity index 100% rename from regression/goto-cc-cbmc-shared-options/readme.md rename to regression/goto-cc-cbmc-shared-options/README.md diff --git a/regression/symtab2gb-cbmc/readme.md b/regression/symtab2gb-cbmc/README.md similarity index 100% rename from regression/symtab2gb-cbmc/readme.md rename to regression/symtab2gb-cbmc/README.md diff --git a/regression/symtab2gb/readme.md b/regression/symtab2gb/README.md similarity index 100% rename from regression/symtab2gb/readme.md rename to regression/symtab2gb/README.md diff --git a/scripts/bash-autocomplete/Readme.md b/scripts/bash-autocomplete/README.md similarity index 100% rename from scripts/bash-autocomplete/Readme.md rename to scripts/bash-autocomplete/README.md From 91c7e81edd3ac282f6543638c4e442e7627298df Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 15 Nov 2022 14:27:46 +0000 Subject: [PATCH 2/3] Include a reference to test tags in our documentation regression/README.md describes the tags, but wasn't referenced from anywhere. --- doc/architectural/compilation-and-development.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/doc/architectural/compilation-and-development.md b/doc/architectural/compilation-and-development.md index 0bce414fd6a..4816d373afa 100644 --- a/doc/architectural/compilation-and-development.md +++ b/doc/architectural/compilation-and-development.md @@ -77,6 +77,12 @@ CI, should succeed), `THOROUGH` (takes too long to be run in CI, should succeed), `FUTURE` (will succeed when a planned feature is added) or `KNOWNBUG` (will succeed when a bug is fixed). +Test descriptions may also include a number of tags. `test.pl -I` will only +run tests with a particular ``, and `test.pl -X` will run all tests +except for those with a particular ``. See +[regression/README.md](https://github.com/diffblue/cbmc/blob/develop/regression/README.md) +for the current set of tags and their intended use. + \subsubsection compilation-and-development-subsubsection-running-regression-tests-with-make Running regression tests with make If you have compiled using `make` then you can run the regression tests From 107ff858edf6dc0670827e29405fe5f5a598389d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 15 Nov 2022 14:35:07 +0000 Subject: [PATCH 3/3] Remove any remaining references to Travis CI Removes links that are no longer relevant and adds clarifying notes where we previously had errors pending investigation. --- regression/README.md | 13 +++---------- .../test.desc | 4 +--- 2 files changed, 4 insertions(+), 13 deletions(-) diff --git a/regression/README.md b/regression/README.md index 218f51a8763..54baab0cf94 100644 --- a/regression/README.md +++ b/regression/README.md @@ -30,13 +30,6 @@ This folder contains the CProver regression test-suite. - `winbug`: These tests are currently known to be failing on Windows, - but passing on other platforms. - The reason for this is not known, and it's currently being investigated. - This was discovered during work done to port CI from [Travis] - and [AWS CodeBuild] to [GitHub Actions]. - Worth noting that those tests were not being run on Windows before. - - -[AWS CodeBuild]: https://aws.amazon.com/codebuild/ -[GitHub Actions]: https://github.com/features/actions -[Travis]: https://travis-ci.com/ + but passing on other platforms. https://github.com/diffblue/cbmc/pull/5572 + will address one part thereof; the remaining ones are C++ tests that fail on + both Windows and MacOS for our lack of C++-11 support. diff --git a/regression/goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries/test.desc b/regression/goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries/test.desc index 77516db1ccb..ac805176c57 100644 --- a/regression/goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries/test.desc +++ b/regression/goto-cc-cbmc/malloc-may-fail-should-work-with-compiled-binaries/test.desc @@ -3,9 +3,7 @@ test.c --malloc-may-fail --malloc-fail-null ^EXIT=10$ ^SIGNAL=0$ -\[main.assertion.1\] line 7 assertion array != .*: FAILURE +\[main.assertion.1\] line 7 assertion array != NULL: FAILURE -- -- Compiling a file with goto-cc should not affect how --malloc-may-fail behaves -Regex in the assertion because on travis for some reason the preprocessor seems to run -before cbmc.