Rename cbmc test suite (now rmc) (#526)

Author: adpaco-aws

README.md

@@ -15,7 +15,7 @@ ignore = [
     # (and generally rustfmt can move around comments in UI-testing incompatible ways)
     "src/test/*",
     "!src/test/cargo-rmc",
-    "!src/test/cbmc",
+    "!src/test/rmc",
     "!src/test/expected",
     "!src/test/firecracker",
     "!src/test/prusti",

rustfmt.toml

@@ -22,8 +22,8 @@ check-cbmc-viewer-version.py --major 2 --minor 5
 
 # Standalone rmc tests, expected tests, and cargo tests
 ./x.py build -i --stage 1 library/std ${EXTRA_X_PY_BUILD_ARGS}
-./x.py test -i --stage 1 cbmc firecracker prusti smack expected cargo-rmc
-./x.py test -i --stage 0 compiler/rustc_codegen_llvm
+./x.py test -i --stage 1 rmc firecracker prusti smack expected cargo-rmc
+./x.py test -i --stage 0 compiler/cbmc
 
 # Check codegen for the standard library
 $SCRIPT_DIR/std-lib-regression.sh

scripts/rmc-regression.sh

@@ -24,6 +24,6 @@ export PATH=$SCRIPT_DIR:$PATH
 RMC_DIR=$SCRIPT_DIR/..
 
 find $RMC_DIR/library/rmc -name "*.c" | xargs clang-format $FLAGS
-find $RMC_DIR/src/test/cbmc -name "*.c" | xargs clang-format $FLAGS
+find $RMC_DIR/src/test/rmc -name "*.c" | xargs clang-format $FLAGS
 find $RMC_DIR/src/test/cargo-rmc -name "*.c" | xargs clang-format $FLAGS
 

scripts/run-clang-format.sh

@@ -464,7 +464,7 @@ impl<'a> Builder<'a> {
                 // Run bootstrap close to the end as it's unlikely to fail
                 test::Bootstrap,
                 // RMC regression tests
-                test::CBMC,
+                test::RMC,
                 test::Firecracker,
                 test::Prusti,
                 test::Serial,

src/bootstrap/builder.rs

@@ -1205,7 +1205,7 @@ host_test!(RunMakeFullDeps {
 
 default_test!(Assembly { path: "src/test/assembly", mode: "assembly", suite: "assembly" });
 
-default_test!(CBMC { path: "src/test/cbmc", mode: "rmc", suite: "cbmc" });
+default_test!(RMC { path: "src/test/rmc", mode: "rmc", suite: "rmc" });
 
 default_test!(Firecracker { path: "src/test/firecracker", mode: "rmc", suite: "firecracker" });
 

src/bootstrap/test.rs

@@ -6,7 +6,7 @@
 include!("../../rmc-prelude.rs");
 
 // This example is a copy of the `cbmc` test in
-// `src/test/cbmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs`
+// `src/test/rmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs`
 //
 // The verification output should show an unwinding assertion failure.
 //