Clarify Rust intrinsic assumption error message (#4015)

"assumption failed" is mysterious--the user will likely conclude that a
`kani::assume` failed, when in fact this is an assume introduced by the
Rust compiler to perform optimizations.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: Carolyn Zech

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -299,7 +299,7 @@ impl GotocCtx<'_> {
             Intrinsic::Assume => self.codegen_assert_assume(
                 fargs.remove(0).cast_to(Type::bool()),
                 PropertyClass::Assume,
-                "assumption failed",
+                "Rust intrinsic assumption failed",
                 loc,
             ),
             Intrinsic::AtomicAnd(_) => codegen_atomic_binop!(bitand),

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

@@ -151,12 +151,15 @@ impl GotocCtx<'_> {
                 let farg_types = operands.map(|op| self.operand_ty_stable(&op));
                 self.codegen_copy("copy_nonoverlapping", true, fargs, &farg_types, None, location)
             }
+            // https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.NonDivergingIntrinsic.html#variant.Assume
+            // Informs the optimizer that a condition is always true.
+            // If the condition is false, the behavior is undefined.
             StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(ref op)) => {
                 let cond = self.codegen_operand_stable(op).cast_to(Type::bool());
                 self.codegen_assert_assume(
                     cond,
                     PropertyClass::Assume,
-                    "assumption failed",
+                    "Rust intrinsic assumption failed",
                     location,
                 )
             }

tests/expected/any_vec/exact_length.expected

@@ -1,11 +1,11 @@
 Checking harness check_access_length_17...
 
-Failed Checks: assumption failed\
+Failed Checks: Rust intrinsic assumption failed\
 in <usize as std::slice::SliceIndex<[u8]>>::get_unchecked
 
 Checking harness check_access_length_zero...
 
-Failed Checks: assumption failed\
+Failed Checks: Rust intrinsic assumption failed\
 in <usize as std::slice::SliceIndex<[u8]>>::get_unchecked
 
 Verification failed for - check_access_length_17

tests/expected/any_vec/out_bounds.expected

@@ -1,6 +1,6 @@
 Checking harness check_always_out_bounds...
 
-Failed Checks: assumption failed
+Failed Checks: Rust intrinsic assumption failed
 in <usize as std::slice::SliceIndex<[u8]>>::get_unchecked
 
 Verification failed for - check_always_out_bounds