Rename cbmc test suite (now rmc)

README.md

@@ -45,7 +45,7 @@ Until then, the easiest way to use RMC is as follows
 
 1. Add `rmc/scripts` to your path
 1. Go to a folder that contains a rust file you would like to verify with RMC.
-   For example, `cd rmc/src/test/cbmc/Parenths`.
+   For example, `cd rmc/src/test/rmc/Parenths`.
    By default, `rmc` uses `main()` as the entry point.
 1. Execute RMC on the file
    ```
@@ -98,7 +98,7 @@ Lastly, you can override specific flags from command line, e.g. with `cargo rmc
 ### Advanced flags
 RMC supports a set of advanced flags that give you control over the verification process.
 For example, consider the `CopyIntrinsics` regression test:
-1. `cd rmc/src/test/cbmc/CopyIntrinsics`
+1. `cd rmc/src/test/rmc/CopyIntrinsics`
 1. Execute RMC on the file
    `rmc main.rs`
 1. Note that this will unwind forever

rustfmt.toml

@@ -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",

scripts/rmc-regression.sh

@@ -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/run-clang-format.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
 

src/bootstrap/builder.rs

@@ -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/test.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/test/expected/unwind_tip/main.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.
 //

src/test/cbmc/ForeignItems/main.rs → src/test/rmc/ForeignItems/main.rs

@@ -3,7 +3,7 @@
 //! To run this test, do
 //! rmc main.rs -- lib.c
 
-// rmc-flags: --c-lib src/test/cbmc/ForeignItems/lib.c
+// rmc-flags: --c-lib src/test/rmc/ForeignItems/lib.c
 
 #[repr(C)]
 pub struct Foo {