Consistently name README files and clean up

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<tag>` will only
+run tests with a particular `<tag>`, and `test.pl -X<tag>` will run all tests
+except for those with a particular `<tag>`. 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

regression/readme.md → 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.

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.