Fix unreachable code handling (rust-lang#540).

Our codegen for unreachable statements were incorrect. CBMC doesn't
treat assert(0) as a terminal instruction. This was causing CBMC to get
stuck in a false loop.

Instead, we should generate an assertion followed by an assumption to
guarantee that CBMC would end there.

compiler/rustc_codegen_rmc/src/codegen/statement.rs

@@ -56,7 +56,13 @@ impl<'tcx> GotocCtx<'tcx> {
                     }
                 }
             }
-            TerminatorKind::Unreachable => Stmt::assert_false("unreachable code", loc),
+            TerminatorKind::Unreachable => Stmt::block(
+                vec![
+                    Stmt::assert_false("unreachable code", loc.clone()),
+                    Stmt::assume(Expr::bool_false(), loc.clone()),
+                ],
+                loc,
+            ),
             TerminatorKind::Drop { place, target, unwind: _ } => self.codegen_drop(place, target),
             TerminatorKind::DropAndReplace { .. } => {
                 unreachable!("this instruction is unreachable")

src/test/rmc/Enum/result3.rs

@@ -1,9 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// There is an implicit loop inside PartialEq, so we need an explicit unwind
-// cbmc-flags: --unwind 3 --unwinding-assertions
-
 include!("../../rmc-prelude.rs");
 
 #[derive(Debug, PartialEq)]