diff --git a/.github/workflows/copyright.yml b/.github/workflows/copyright.yml
index 054cf65ffb438..7f8c35c7cee7a 100644
--- a/.github/workflows/copyright.yml
+++ b/.github/workflows/copyright.yml
@@ -15,7 +15,7 @@ jobs:
       - name: Get paths for files added
         id: git-diff
         run: |
-          files=$(git diff --name-only --diff-filter=A ${{ github.event.pull_request.base.sha }} ${{ github.event.pull_request.head.sha }} | xargs)
+          files=$(git diff --name-only --diff-filter=A ${{ github.event.pull_request.base.sha }} ${{ github.event.pull_request.head.sha }} | grep -v -E '(expected|gitignore)$' | xargs)
           echo "::set-output name=paths::$files"
 
       - name: Execute copyright check
diff --git a/scripts/rmc-regression.sh b/scripts/rmc-regression.sh
index 1320da89091a0..880a9616c54a8 100755
--- a/scripts/rmc-regression.sh
+++ b/scripts/rmc-regression.sh
@@ -9,8 +9,6 @@ set -o pipefail
 set -o nounset
 
 SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
-RUST_DIR=$SCRIPT_DIR/..
-export RMC_RUSTC=`find $RUST_DIR/build -name "rustc" -print | grep stage1`
 export PATH=$SCRIPT_DIR:$PATH
 EXTRA_X_PY_BUILD_ARGS="${EXTRA_X_PY_BUILD_ARGS:-}"
 
@@ -21,10 +19,6 @@ check-cbmc-viewer-version.py --major 2 --minor 5
 # Formatting check
 ./x.py fmt --check
 
-# Standalone rmc tests and cargo tests
-pushd $RUST_DIR
+# 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 cargo-rmc
-
-# run-make tests
-./x.py test -i --stage 1 src/test/run-make --test-args gotoc
+./x.py test -i --stage 1 cbmc firecracker prusti smack expected cargo-rmc
diff --git a/src/bootstrap/builder.rs b/src/bootstrap/builder.rs
index 9c54bb86f3ab7..20373982eabbe 100644
--- a/src/bootstrap/builder.rs
+++ b/src/bootstrap/builder.rs
@@ -469,6 +469,7 @@ impl<'a> Builder<'a> {
                 test::Serial,
                 test::SMACK,
                 test::CargoRMC,
+                test::Expected,
                 // Run run-make last, since these won't pass without make on Windows
                 test::RunMake,
             ),
diff --git a/src/bootstrap/test.rs b/src/bootstrap/test.rs
index ad0312fb1b991..481e9de7a77a7 100644
--- a/src/bootstrap/test.rs
+++ b/src/bootstrap/test.rs
@@ -1212,6 +1212,8 @@ default_test!(SMACK { path: "src/test/smack", mode: "rmc", suite: "smack" });
 
 default_test!(CargoRMC { path: "src/test/cargo-rmc", mode: "cargo-rmc", suite: "cargo-rmc" });
 
+default_test!(Expected { path: "src/test/expected", mode: "expected", suite: "expected" });
+
 #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
 struct Compiletest {
     compiler: Compiler,
diff --git a/src/test/run-make/gotoc-allocation/expected b/src/test/expected/allocation/expected
similarity index 100%
rename from src/test/run-make/gotoc-allocation/expected
rename to src/test/expected/allocation/expected
diff --git a/src/test/run-make/gotoc-allocation/main.rs b/src/test/expected/allocation/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-allocation/main.rs
rename to src/test/expected/allocation/main.rs
diff --git a/src/test/run-make/gotoc-array/expected b/src/test/expected/array/expected
similarity index 56%
rename from src/test/run-make/gotoc-array/expected
rename to src/test/expected/array/expected
index 3c12b195ab5b2..70152d4c1d60c 100644
--- a/src/test/run-make/gotoc-array/expected
+++ b/src/test/expected/array/expected
@@ -3,7 +3,7 @@ array 'y'.0 upper bound in y.0[var_12]: SUCCESS
 array 'y'.0 upper bound in y.0[var_16]: FAILURE
 array 'x'.0 upper bound in x.0[var_3]: SUCCESS
 array 'x'.0 upper bound in x.0[var_5]: SUCCESS
-line 11 assertion failed: y[0] == 1: SUCCESS
-line 12 assertion failed: y[1] == 2: SUCCESS
-line 13 index out of bounds: the length is move _17 but the index is _16: FAILURE
-line 13 assertion failed: y[z] == 3: FAILURE
+line 12 assertion failed: y[0] == 1: SUCCESS
+line 13 assertion failed: y[1] == 2: SUCCESS
+line 14 index out of bounds: the length is move _17 but the index is _16: FAILURE
+line 14 assertion failed: y[z] == 3: FAILURE
diff --git a/src/test/run-make/gotoc-array/main.rs b/src/test/expected/array/main.rs
similarity index 91%
rename from src/test/run-make/gotoc-array/main.rs
rename to src/test/expected/array/main.rs
index b9131fa437a1f..4d65a71968847 100644
--- a/src/test/run-make/gotoc-array/main.rs
+++ b/src/test/expected/array/main.rs
@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// cbmc-flags: --bounds-check
 fn foo(x: [i32; 5]) -> [i32; 2] {
     [x[0], x[1]]
 }
diff --git a/src/test/run-make/gotoc-assert-eq/expected b/src/test/expected/assert-eq/expected
similarity index 100%
rename from src/test/run-make/gotoc-assert-eq/expected
rename to src/test/expected/assert-eq/expected
diff --git a/src/test/run-make/gotoc-assert-eq/main.rs b/src/test/expected/assert-eq/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-assert-eq/main.rs
rename to src/test/expected/assert-eq/main.rs
diff --git a/src/test/run-make/gotoc-binop/expected b/src/test/expected/binop/expected
similarity index 100%
rename from src/test/run-make/gotoc-binop/expected
rename to src/test/expected/binop/expected
diff --git a/src/test/run-make/gotoc-binop/main.rs b/src/test/expected/binop/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-binop/main.rs
rename to src/test/expected/binop/main.rs
diff --git a/src/test/expected/closure/expected b/src/test/expected/closure/expected
new file mode 100644
index 0000000000000..d4a3360543de9
--- /dev/null
+++ b/src/test/expected/closure/expected
@@ -0,0 +1,7 @@
+resume instruction: SUCCESS
+line 22 attempt to compute `move _8 + move _9`, which would overflow: SUCCESS
+line 22 attempt to compute `move _5 + move _6`, which would overflow: SUCCESS
+line 22 attempt to compute `(*((*_1).0: &mut i32)) + move _4`, which would overflow: SUCCESS
+line 27 attempt to compute `move _18 + const 12_i32`, which would overflow: SUCCESS
+line 27 assertion failed: original_num + 12 == num: SUCCESS
+line 27 arithmetic overflow on signed + in var_18 + 12: SUCCESS
diff --git a/src/test/run-make/gotoc-closure/main.rs b/src/test/expected/closure/main.rs
similarity index 94%
rename from src/test/run-make/gotoc-closure/main.rs
rename to src/test/expected/closure/main.rs
index 8ac82875ffa8f..3769d678dfe02 100644
--- a/src/test/run-make/gotoc-closure/main.rs
+++ b/src/test/expected/closure/main.rs
@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// cbmc-flags: --signed-overflow-check
 fn call_with_one<F>(mut some_closure: F) -> ()
     where
         F: FnMut(i64, i64) -> (),
diff --git a/src/test/run-make/gotoc-closure2/expected b/src/test/expected/closure2/expected
similarity index 100%
rename from src/test/run-make/gotoc-closure2/expected
rename to src/test/expected/closure2/expected
diff --git a/src/test/run-make/gotoc-closure2/main.rs b/src/test/expected/closure2/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-closure2/main.rs
rename to src/test/expected/closure2/main.rs
diff --git a/src/test/run-make/gotoc-closure3/expected b/src/test/expected/closure3/expected
similarity index 100%
rename from src/test/run-make/gotoc-closure3/expected
rename to src/test/expected/closure3/expected
diff --git a/src/test/run-make/gotoc-closure3/main.rs b/src/test/expected/closure3/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-closure3/main.rs
rename to src/test/expected/closure3/main.rs
diff --git a/src/test/run-make/gotoc-comp/expected b/src/test/expected/comp/expected
similarity index 100%
rename from src/test/run-make/gotoc-comp/expected
rename to src/test/expected/comp/expected
diff --git a/src/test/run-make/gotoc-comp/main.rs b/src/test/expected/comp/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-comp/main.rs
rename to src/test/expected/comp/main.rs
diff --git a/src/test/run-make/gotoc-copy/expected b/src/test/expected/copy/expected
similarity index 100%
rename from src/test/run-make/gotoc-copy/expected
rename to src/test/expected/copy/expected
diff --git a/src/test/run-make/gotoc-copy/main.rs b/src/test/expected/copy/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-copy/main.rs
rename to src/test/expected/copy/main.rs
diff --git a/src/test/run-make/gotoc-dynamic-error-trait/expected b/src/test/expected/dynamic-error-trait/expected
similarity index 100%
rename from src/test/run-make/gotoc-dynamic-error-trait/expected
rename to src/test/expected/dynamic-error-trait/expected
diff --git a/src/test/run-make/gotoc-dynamic-error-trait/main.rs b/src/test/expected/dynamic-error-trait/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-dynamic-error-trait/main.rs
rename to src/test/expected/dynamic-error-trait/main.rs
diff --git a/src/test/run-make/gotoc-dynamic-trait-static-dispatch/expected b/src/test/expected/dynamic-trait-static-dispatch/expected
similarity index 100%
rename from src/test/run-make/gotoc-dynamic-trait-static-dispatch/expected
rename to src/test/expected/dynamic-trait-static-dispatch/expected
diff --git a/src/test/run-make/gotoc-dynamic-trait-static-dispatch/main.rs b/src/test/expected/dynamic-trait-static-dispatch/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-dynamic-trait-static-dispatch/main.rs
rename to src/test/expected/dynamic-trait-static-dispatch/main.rs
diff --git a/src/test/run-make/gotoc-dynamic-trait/expected b/src/test/expected/dynamic-trait/expected
similarity index 100%
rename from src/test/run-make/gotoc-dynamic-trait/expected
rename to src/test/expected/dynamic-trait/expected
diff --git a/src/test/run-make/gotoc-dynamic-trait/main.rs b/src/test/expected/dynamic-trait/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-dynamic-trait/main.rs
rename to src/test/expected/dynamic-trait/main.rs
diff --git a/src/test/run-make/gotoc-enum/expected b/src/test/expected/enum/expected
similarity index 100%
rename from src/test/run-make/gotoc-enum/expected
rename to src/test/expected/enum/expected
diff --git a/src/test/run-make/gotoc-enum/main.rs b/src/test/expected/enum/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-enum/main.rs
rename to src/test/expected/enum/main.rs
diff --git a/src/test/run-make/gotoc-float-nan/expected b/src/test/expected/float-nan/expected
similarity index 100%
rename from src/test/run-make/gotoc-float-nan/expected
rename to src/test/expected/float-nan/expected
diff --git a/src/test/run-make/gotoc-float-nan/main.rs b/src/test/expected/float-nan/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-float-nan/main.rs
rename to src/test/expected/float-nan/main.rs
diff --git a/src/test/run-make/gotoc-generics/expected b/src/test/expected/generics/expected
similarity index 100%
rename from src/test/run-make/gotoc-generics/expected
rename to src/test/expected/generics/expected
diff --git a/src/test/run-make/gotoc-generics/main.rs b/src/test/expected/generics/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-generics/main.rs
rename to src/test/expected/generics/main.rs
diff --git a/src/test/run-make/gotoc-iterator/expected b/src/test/expected/iterator/expected
similarity index 100%
rename from src/test/run-make/gotoc-iterator/expected
rename to src/test/expected/iterator/expected
diff --git a/src/test/run-make/gotoc-iterator/main.rs b/src/test/expected/iterator/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-iterator/main.rs
rename to src/test/expected/iterator/main.rs
diff --git a/src/test/run-make/gotoc-niche/expected b/src/test/expected/niche/expected
similarity index 100%
rename from src/test/run-make/gotoc-niche/expected
rename to src/test/expected/niche/expected
diff --git a/src/test/run-make/gotoc-niche/main.rs b/src/test/expected/niche/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-niche/main.rs
rename to src/test/expected/niche/main.rs
diff --git a/src/test/run-make/gotoc-niche2/expected b/src/test/expected/niche2/expected
similarity index 100%
rename from src/test/run-make/gotoc-niche2/expected
rename to src/test/expected/niche2/expected
diff --git a/src/test/run-make/gotoc-niche2/main.rs b/src/test/expected/niche2/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-niche2/main.rs
rename to src/test/expected/niche2/main.rs
diff --git a/src/test/run-make/gotoc-nondet/expected b/src/test/expected/nondet/expected
similarity index 100%
rename from src/test/run-make/gotoc-nondet/expected
rename to src/test/expected/nondet/expected
diff --git a/src/test/run-make/gotoc-nondet/main.rs b/src/test/expected/nondet/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-nondet/main.rs
rename to src/test/expected/nondet/main.rs
diff --git a/src/test/run-make/gotoc-references/expected b/src/test/expected/references/expected
similarity index 100%
rename from src/test/run-make/gotoc-references/expected
rename to src/test/expected/references/expected
diff --git a/src/test/run-make/gotoc-references/main.rs b/src/test/expected/references/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-references/main.rs
rename to src/test/expected/references/main.rs
diff --git a/src/test/expected/replace-hashmap/expected b/src/test/expected/replace-hashmap/expected
new file mode 100644
index 0000000000000..a046c916042bb
--- /dev/null
+++ b/src/test/expected/replace-hashmap/expected
@@ -0,0 +1,6 @@
+line 28 attempt to compute `((*_1).0: usize) + const 1_usize`, which would overflow: SUCCESS
+line 28 arithmetic overflow on unsigned + in self->len + 1: SUCCESS
+line 58 assertion failed: a.is_some(): FAILURE
+line 59 assertion failed: a.is_none(): FAILURE
+line 61 assertion failed: b.is_some(): SUCCESS
+line 62 assertion failed: b.is_none(): FAILURE
diff --git a/src/test/run-make/gotoc-replace-hashmap/main.rs b/src/test/expected/replace-hashmap/main.rs
similarity index 97%
rename from src/test/run-make/gotoc-replace-hashmap/main.rs
rename to src/test/expected/replace-hashmap/main.rs
index decb3eac55613..9f8ea83b0a67a 100644
--- a/src/test/run-make/gotoc-replace-hashmap/main.rs
+++ b/src/test/expected/replace-hashmap/main.rs
@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// cbmc-flags: --unsigned-overflow-check
 use std::collections::HashMap;
 use std::hash::Hash;
 use std::collections::hash_map::RandomState;
diff --git a/src/test/run-make/gotoc-replace-vec/expected b/src/test/expected/replace-vec/expected
similarity index 100%
rename from src/test/run-make/gotoc-replace-vec/expected
rename to src/test/expected/replace-vec/expected
diff --git a/src/test/run-make/gotoc-replace-vec/main.rs b/src/test/expected/replace-vec/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-replace-vec/main.rs
rename to src/test/expected/replace-vec/main.rs
diff --git a/src/test/run-make/gotoc-slice/expected b/src/test/expected/slice/expected
similarity index 100%
rename from src/test/run-make/gotoc-slice/expected
rename to src/test/expected/slice/expected
diff --git a/src/test/run-make/gotoc-slice/main.rs b/src/test/expected/slice/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-slice/main.rs
rename to src/test/expected/slice/main.rs
diff --git a/src/test/run-make/gotoc-static-mutable-struct/expected b/src/test/expected/static-mutable-struct/expected
similarity index 100%
rename from src/test/run-make/gotoc-static-mutable-struct/expected
rename to src/test/expected/static-mutable-struct/expected
diff --git a/src/test/run-make/gotoc-static-mutable-struct/main.rs b/src/test/expected/static-mutable-struct/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-static-mutable-struct/main.rs
rename to src/test/expected/static-mutable-struct/main.rs
diff --git a/src/test/run-make/gotoc-static-mutable/expected b/src/test/expected/static-mutable/expected
similarity index 100%
rename from src/test/run-make/gotoc-static-mutable/expected
rename to src/test/expected/static-mutable/expected
diff --git a/src/test/run-make/gotoc-static-mutable/main.rs b/src/test/expected/static-mutable/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-static-mutable/main.rs
rename to src/test/expected/static-mutable/main.rs
diff --git a/src/test/run-make/gotoc-static/expected b/src/test/expected/static/expected
similarity index 100%
rename from src/test/run-make/gotoc-static/expected
rename to src/test/expected/static/expected
diff --git a/src/test/run-make/gotoc-static/main.rs b/src/test/expected/static/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-static/main.rs
rename to src/test/expected/static/main.rs
diff --git a/src/test/run-make/gotoc-test1/expected b/src/test/expected/test1/expected
similarity index 100%
rename from src/test/run-make/gotoc-test1/expected
rename to src/test/expected/test1/expected
diff --git a/src/test/run-make/gotoc-test1/main.rs b/src/test/expected/test1/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-test1/main.rs
rename to src/test/expected/test1/main.rs
diff --git a/src/test/run-make/gotoc-test2/expected b/src/test/expected/test2/expected
similarity index 100%
rename from src/test/run-make/gotoc-test2/expected
rename to src/test/expected/test2/expected
diff --git a/src/test/run-make/gotoc-test2/main.rs b/src/test/expected/test2/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-test2/main.rs
rename to src/test/expected/test2/main.rs
diff --git a/src/test/run-make/gotoc-test3/expected b/src/test/expected/test3/expected
similarity index 100%
rename from src/test/run-make/gotoc-test3/expected
rename to src/test/expected/test3/expected
diff --git a/src/test/run-make/gotoc-test3/main.rs b/src/test/expected/test3/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-test3/main.rs
rename to src/test/expected/test3/main.rs
diff --git a/src/test/run-make/gotoc-test4/expected b/src/test/expected/test4/expected
similarity index 100%
rename from src/test/run-make/gotoc-test4/expected
rename to src/test/expected/test4/expected
diff --git a/src/test/run-make/gotoc-test4/main.rs b/src/test/expected/test4/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-test4/main.rs
rename to src/test/expected/test4/main.rs
diff --git a/src/test/run-make/gotoc-test5/expected b/src/test/expected/test5/expected
similarity index 100%
rename from src/test/run-make/gotoc-test5/expected
rename to src/test/expected/test5/expected
diff --git a/src/test/run-make/gotoc-test5/main.rs b/src/test/expected/test5/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-test5/main.rs
rename to src/test/expected/test5/main.rs
diff --git a/src/test/run-make/gotoc-test6/expected b/src/test/expected/test6/expected
similarity index 100%
rename from src/test/run-make/gotoc-test6/expected
rename to src/test/expected/test6/expected
diff --git a/src/test/run-make/gotoc-test6/main.rs b/src/test/expected/test6/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-test6/main.rs
rename to src/test/expected/test6/main.rs
diff --git a/src/test/run-make/gotoc-transmute/expected b/src/test/expected/transmute/expected
similarity index 100%
rename from src/test/run-make/gotoc-transmute/expected
rename to src/test/expected/transmute/expected
diff --git a/src/test/run-make/gotoc-transmute/main.rs b/src/test/expected/transmute/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-transmute/main.rs
rename to src/test/expected/transmute/main.rs
diff --git a/src/test/run-make/gotoc-vec/expected b/src/test/expected/vec/expected
similarity index 100%
rename from src/test/run-make/gotoc-vec/expected
rename to src/test/expected/vec/expected
diff --git a/src/test/run-make/gotoc-vec/main.rs b/src/test/expected/vec/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-vec/main.rs
rename to src/test/expected/vec/main.rs
diff --git a/src/test/run-make/gotoc-vecdq/expected b/src/test/expected/vecdq/expected
similarity index 100%
rename from src/test/run-make/gotoc-vecdq/expected
rename to src/test/expected/vecdq/expected
diff --git a/src/test/run-make/gotoc-vecdq/main.rs b/src/test/expected/vecdq/main.rs
similarity index 100%
rename from src/test/run-make/gotoc-vecdq/main.rs
rename to src/test/expected/vecdq/main.rs
diff --git a/src/test/run-make/Makefile.common b/src/test/run-make/Makefile.common
deleted file mode 100644
index 6131a1f916052..0000000000000
--- a/src/test/run-make/Makefile.common
+++ /dev/null
@@ -1,14 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
-SHELL=/bin/bash
-
-CBMC_ARGS=\
-    --object-bits 11 \
-    --signed-overflow-check \
-    --unsigned-overflow-check \
-    --bounds-check \
-    --pointer-check
-
-all:
-	rmc --allow-cbmc-verification-failure main.rs -- $(CBMC_ARGS) 2>&1 | tee $(TMPDIR)output; exit $${PIPESTATUS[0]}
-	../compare-output.sh expected $(TMPDIR)output
diff --git a/src/test/run-make/compare-output.sh b/src/test/run-make/compare-output.sh
deleted file mode 100755
index 7a7f36c0ebb52..0000000000000
--- a/src/test/run-make/compare-output.sh
+++ /dev/null
@@ -1,11 +0,0 @@
-#!/bin/bash
-
-LINES=$1
-FILE=$2
-
-while IFS= read -r line; do
-    if ! grep -q -F "$line" "$FILE"; then
-        echo "This line doesn't exist: $line"
-        exit 1
-    fi
-done < "$LINES"
diff --git a/src/test/run-make/gotoc-allocation/Makefile b/src/test/run-make/gotoc-allocation/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-allocation/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-array/Makefile b/src/test/run-make/gotoc-array/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-array/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-assert-eq/Makefile b/src/test/run-make/gotoc-assert-eq/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-assert-eq/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-binop/Makefile b/src/test/run-make/gotoc-binop/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-binop/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-closure/Makefile b/src/test/run-make/gotoc-closure/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-closure/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-closure/expected b/src/test/run-make/gotoc-closure/expected
deleted file mode 100644
index b0d3d687fb760..0000000000000
--- a/src/test/run-make/gotoc-closure/expected
+++ /dev/null
@@ -1,7 +0,0 @@
-resume instruction: SUCCESS
-line 21 attempt to compute `move _8 + move _9`, which would overflow: SUCCESS
-line 21 attempt to compute `move _5 + move _6`, which would overflow: SUCCESS
-line 21 attempt to compute `(*((*_1).0: &mut i32)) + move _4`, which would overflow: SUCCESS
-line 26 attempt to compute `move _18 + const 12_i32`, which would overflow: SUCCESS
-line 26 assertion failed: original_num + 12 == num: SUCCESS
-line 26 arithmetic overflow on signed + in var_18 + 12: SUCCESS
diff --git a/src/test/run-make/gotoc-closure2/Makefile b/src/test/run-make/gotoc-closure2/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-closure2/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-closure3/Makefile b/src/test/run-make/gotoc-closure3/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-closure3/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-comp/Makefile b/src/test/run-make/gotoc-comp/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-comp/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-copy/Makefile b/src/test/run-make/gotoc-copy/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-copy/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-dynamic-error-trait/Makefile b/src/test/run-make/gotoc-dynamic-error-trait/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-dynamic-error-trait/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-dynamic-trait-static-dispatch/Makefile b/src/test/run-make/gotoc-dynamic-trait-static-dispatch/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-dynamic-trait-static-dispatch/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-dynamic-trait/Makefile b/src/test/run-make/gotoc-dynamic-trait/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-dynamic-trait/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-enum/Makefile b/src/test/run-make/gotoc-enum/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-enum/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-float-nan/Makefile b/src/test/run-make/gotoc-float-nan/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-float-nan/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-generics/Makefile b/src/test/run-make/gotoc-generics/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-generics/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-iterator/Makefile b/src/test/run-make/gotoc-iterator/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-iterator/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-multifile/Makefile b/src/test/run-make/gotoc-multifile/Makefile
deleted file mode 100644
index d69ff119dfd10..0000000000000
--- a/src/test/run-make/gotoc-multifile/Makefile
+++ /dev/null
@@ -1,12 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-
-all:
-	$(RUSTC) foo.rs
-	$(RUSTC) -Z codegen-backend=gotoc foo.rs
-	symtab2gb $(TMPDIR)/foo.json --out $(TMPDIR)/foo.o
-	$(RUSTC) -Z codegen-backend=gotoc bar.rs
-	symtab2gb $(TMPDIR)/bar.json --out $(TMPDIR)/bar.o
-	goto-cc $(TMPDIR)/foo.o $(TMPDIR)/bar.o -o $(TMPDIR)/mix
-
diff --git a/src/test/run-make/gotoc-multifile/bar.rs b/src/test/run-make/gotoc-multifile/bar.rs
deleted file mode 100644
index 8fea239e2b7c6..0000000000000
--- a/src/test/run-make/gotoc-multifile/bar.rs
+++ /dev/null
@@ -1,8 +0,0 @@
-// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-#![no_std]
-#![crate_type = "lib"]
-
-extern crate foo;
-
-pub fn bar() -> foo::A { foo::foo() }
diff --git a/src/test/run-make/gotoc-multifile/foo.rs b/src/test/run-make/gotoc-multifile/foo.rs
deleted file mode 100644
index 8b0e1f00364f5..0000000000000
--- a/src/test/run-make/gotoc-multifile/foo.rs
+++ /dev/null
@@ -1,15 +0,0 @@
-// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-#![no_std]
-#![crate_type = "lib"]
-
-#[allow(dead_code)]
-pub struct A {
-    x: i32,
-}
-
-pub fn foo() -> A {
-    A {
-        x: 10,
-    }
-}
\ No newline at end of file
diff --git a/src/test/run-make/gotoc-niche/Makefile b/src/test/run-make/gotoc-niche/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-niche/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-niche2/Makefile b/src/test/run-make/gotoc-niche2/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-niche2/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-nondet/Makefile b/src/test/run-make/gotoc-nondet/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-nondet/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-references/Makefile b/src/test/run-make/gotoc-references/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-references/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-replace-hashmap/Makefile b/src/test/run-make/gotoc-replace-hashmap/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-replace-hashmap/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-replace-hashmap/expected b/src/test/run-make/gotoc-replace-hashmap/expected
deleted file mode 100644
index 7fdfb24b2524d..0000000000000
--- a/src/test/run-make/gotoc-replace-hashmap/expected
+++ /dev/null
@@ -1,6 +0,0 @@
-line 27 attempt to compute `((*_1).0: usize) + const 1_usize`, which would overflow: SUCCESS
-line 27 arithmetic overflow on unsigned + in self->len + 1: SUCCESS
-line 57 assertion failed: a.is_some(): FAILURE
-line 58 assertion failed: a.is_none(): FAILURE
-line 60 assertion failed: b.is_some(): SUCCESS
-line 61 assertion failed: b.is_none(): FAILURE
diff --git a/src/test/run-make/gotoc-replace-vec/Makefile b/src/test/run-make/gotoc-replace-vec/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-replace-vec/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-slice/Makefile b/src/test/run-make/gotoc-slice/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-slice/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-static-mutable-struct/Makefile b/src/test/run-make/gotoc-static-mutable-struct/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-static-mutable-struct/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-static-mutable/Makefile b/src/test/run-make/gotoc-static-mutable/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-static-mutable/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-static/Makefile b/src/test/run-make/gotoc-static/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-static/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-test1/Makefile b/src/test/run-make/gotoc-test1/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-test1/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-test2/Makefile b/src/test/run-make/gotoc-test2/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-test2/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-test3/Makefile b/src/test/run-make/gotoc-test3/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-test3/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-test4/Makefile b/src/test/run-make/gotoc-test4/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-test4/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-test5/Makefile b/src/test/run-make/gotoc-test5/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-test5/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-test6/Makefile b/src/test/run-make/gotoc-test6/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-test6/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-transmute/Makefile b/src/test/run-make/gotoc-transmute/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-transmute/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-vec/Makefile b/src/test/run-make/gotoc-vec/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-vec/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/gotoc-vecdq/Makefile b/src/test/run-make/gotoc-vecdq/Makefile
deleted file mode 100644
index 09a85853900b4..0000000000000
--- a/src/test/run-make/gotoc-vecdq/Makefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: Apache-2.0 OR MIT
--include ../../run-make-fulldeps/tools.mk
-include ../Makefile.common
-
diff --git a/src/test/run-make/run-cbmc.sh b/src/test/run-make/run-cbmc.sh
deleted file mode 100755
index 96ccda6d53438..0000000000000
--- a/src/test/run-make/run-cbmc.sh
+++ /dev/null
@@ -1,11 +0,0 @@
-#!/bin/bash
-
-set -x
-
-DIR=$1
-INPUT=$2
-OUTPUT=${2/%.rs/}
-TMPFILE=$3
-FUNC=${4:-main}
-symtab2gb "$DIR/${OUTPUT}.json" --out "$DIR/$OUTPUT" >/dev/null 2>&1 || exit 100
-cbmc $CBMC_EXTRA_FLAGS --object-bits 11 --signed-overflow-check --unsigned-overflow-check --function "$FUNC" "$DIR/$OUTPUT" > "$DIR/$TMPFILE" || true
diff --git a/src/tools/compiletest/src/common.rs b/src/tools/compiletest/src/common.rs
index afc84ff0ebe54..00bea20130ed3 100644
--- a/src/tools/compiletest/src/common.rs
+++ b/src/tools/compiletest/src/common.rs
@@ -25,6 +25,7 @@ pub enum Mode {
     Assembly,
     RMC,
     CargoRMC,
+    Expected,
 }
 
 impl Mode {
@@ -57,6 +58,7 @@ impl FromStr for Mode {
             "assembly" => Ok(Assembly),
             "rmc" => Ok(RMC),
             "cargo-rmc" => Ok(CargoRMC),
+            "expected" => Ok(Expected),
             _ => Err(()),
         }
     }
@@ -80,6 +82,7 @@ impl fmt::Display for Mode {
             Assembly => "assembly",
             RMC => "rmc",
             CargoRMC => "cargo-rmc",
+            Expected => "expected",
         };
         fmt::Display::fmt(s, f)
     }
diff --git a/src/tools/compiletest/src/main.rs b/src/tools/compiletest/src/main.rs
index 7098d2406c96b..9aef777797fba 100644
--- a/src/tools/compiletest/src/main.rs
+++ b/src/tools/compiletest/src/main.rs
@@ -76,7 +76,7 @@ pub fn parse_config(args: Vec<String>) -> Config {
             "mode",
             "which sort of compile tests to run",
             "run-pass-valgrind | pretty | debug-info | codegen | rustdoc \
-            | rustdoc-json | codegen-units | incremental | run-make | ui | js-doc-test | mir-opt | assembly | rmc | cargo-rmc",
+            | rustdoc-json | codegen-units | incremental | run-make | ui | js-doc-test | mir-opt | assembly | rmc | cargo-rmc | expected",
         )
         .reqopt(
             "",
diff --git a/src/tools/compiletest/src/runtest.rs b/src/tools/compiletest/src/runtest.rs
index d0309437554ca..0ce7726d85556 100644
--- a/src/tools/compiletest/src/runtest.rs
+++ b/src/tools/compiletest/src/runtest.rs
@@ -3,7 +3,7 @@
 use crate::common::{expected_output_path, UI_EXTENSIONS, UI_FIXED, UI_STDERR, UI_STDOUT};
 use crate::common::{output_base_dir, output_base_name, output_testname_unique};
 use crate::common::{
-    Assembly, CargoRMC, Incremental, JsDocTest, MirOpt, RunMake, RustdocJson, Ui, RMC,
+    Assembly, CargoRMC, Expected, Incremental, JsDocTest, MirOpt, RunMake, RustdocJson, Ui, RMC,
 };
 use crate::common::{Codegen, CodegenUnits, DebugInfo, Debugger, Rustdoc};
 use crate::common::{CompareMode, FailMode, PassMode};
@@ -355,6 +355,7 @@ impl<'test> TestCx<'test> {
             JsDocTest => self.run_js_doc_test(),
             RMC => self.run_rmc_test(),
             CargoRMC => self.run_cargo_rmc_test(),
+            Expected => self.run_expected_test(),
         }
     }
 
@@ -2026,7 +2027,7 @@ impl<'test> TestCx<'test> {
                 rustc.arg(dir_opt);
             }
             RunPassValgrind | Pretty | DebugInfo | Codegen | Rustdoc | RustdocJson | RunMake
-            | CodegenUnits | JsDocTest | Assembly | RMC | CargoRMC => {
+            | CodegenUnits | JsDocTest | Assembly | RMC | CargoRMC | Expected => {
                 // do not use JSON output
             }
         }
@@ -2430,7 +2431,7 @@ impl<'test> TestCx<'test> {
     }
 
     /// Runs cargo-rmc on the function specified by the stem of `self.testpaths.file`.
-    /// An error message is printed to stdout if verification result does not
+    /// An error message is printed to stdout if verification output does not
     /// contain the expected output in `self.testpaths.file`.
     fn run_cargo_rmc_test(&self) {
         // We create our own command for the same reasons listed in `run_rmc_test` method.
@@ -2449,7 +2450,30 @@ impl<'test> TestCx<'test> {
         self.add_rmc_dir_to_path(&mut cargo);
         let proc_res = self.compose_and_run_compiler(cargo, None);
         let expected = fs::read_to_string(self.testpaths.file.clone()).unwrap();
-        // Print an error if the verification result does not contains the expected lines.
+        self.verify_output(&proc_res, &expected);
+    }
+
+    /// Runs RMC on the test file specified by `self.testpaths.file`. An error
+    /// message is printed to stdout if verification output does not contain
+    /// the expected output in `expected` file.
+    fn run_expected_test(&self) {
+        // We create our own command for the same reasons listed in `run_rmc_test` method.
+        let mut rmc = Command::new("rmc");
+        // Pass the test path along with RMC and CBMC flags parsed from comments at the top of the test file.
+        rmc.args(&self.props.rmc_flags)
+            .arg(&self.testpaths.file)
+            .arg("--")
+            .args(&self.props.cbmc_flags);
+        self.add_rmc_dir_to_path(&mut rmc);
+        let proc_res = self.compose_and_run_compiler(rmc, None);
+        let expected =
+            fs::read_to_string(self.testpaths.file.parent().unwrap().join("expected")).unwrap();
+        self.verify_output(&proc_res, &expected);
+    }
+
+    /// Print an error if the verification output does not contain the expected
+    /// lines.
+    fn verify_output(&self, proc_res: &ProcRes, expected: &str) {
         if let Some(line) = TestCx::contains_lines(&proc_res.stdout, expected.split('\n').collect())
         {
             self.fatal_proc_rec(