Differentiate between check, codegen, and verification errors. (rust-lang#353)

* Differentiate between check, codegen, and verification errors.

* Fix typo.

* Rename tests.

* Address concerns.

* Remove unnecessary code and fix typos.

Author: bdalrhm

src/test/cbmc/Assert/UninitValid/fixme_main_fail.rs renamed to src/test/cbmc/Assert/UninitValid/fixme_main.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 use std::mem::{self, MaybeUninit};
 
 fn main() {

src/test/cbmc/Assert/ZeroValid/fixme_main_fail.rs renamed to src/test/cbmc/Assert/ZeroValid/fixme_main.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 // The function zeroed() calls assert_zero_valid to mark that it is only defined to assign an
 // all-zero bit pattern to a type T if this is a valid value. So the following is undefined.
 

src/test/cbmc/BinOp_Offset/main_fail.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 include!("../../rmc-prelude.rs");
 
 pub fn test_offset_in_double_array() {

src/test/cbmc/BitManipulation/Stable/fixme_main_fail.rs renamed to src/test/cbmc/BitManipulation/Stable/fixme_main.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 fn main() {
     // Intrinsics implemented as integer primitives
     // https://doc.rust-lang.org/core/intrinsics/fn.cttz.html

src/test/cbmc/BitManipulation/Unstable/fixme_main_fail.rs renamed to src/test/cbmc/BitManipulation/Unstable/fixme_main.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
+
 #![feature(core_intrinsics)]
 use std::intrinsics::{ctlz, cttz, cttz_nonzero};
 

src/test/cbmc/Count/Unstable/Ctlz/bounds_fail.rs renamed to src/test/cbmc/Count/Unstable/Ctlz/bounds.rs

@@ -1,6 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-
+// rmc-verify-fail
 // cbmc-flags: --bounds-check
 
 #![feature(core_intrinsics)]

src/test/cbmc/Count/Unstable/Cttz/bounds_fail.rs renamed to src/test/cbmc/Count/Unstable/Cttz/bounds.rs

@@ -1,6 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-
+// rmc-verify-fail
 // cbmc-flags: --bounds-check
 
 #![feature(core_intrinsics)]

src/test/cbmc/DynTrait/boxed_closure_fail_fixme.rs

@@ -1,10 +1,11 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // Check that we can codegen a boxed dyn closure and fail an inner assertion
 
 // This current verifies "successfully" because the closure is not actually
-// called in the resulting CotoC code.
+// called in the resulting GotoC code.
 // https://github.com/model-checking/rmc/issues/240
 
 include!("../../rmc-prelude.rs");

src/test/cbmc/DynTrait/boxed_trait_fail.rs

@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // Dynamic traits should work when used through a box
 // _fail test; all assertions inverted.

src/test/cbmc/DynTrait/different_crates_fail.rs

@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // This test uses a trait defined in a different crate (the standard library)
 // and a test defined in the local crate. The goal is to test vtable resolution