Add tests for forget (rust-lang#1041)

* Disable `forget` intrinsic * Restore `forget` * Add two tests for `forget` * Update `forget` status in support table * Use `check-fail` instead of `codegen-fail`

Author: adpaco-aws

docs/src/rust-feature-support.md

@@ -338,7 +338,7 @@ floorf64 | No | |
 fmaf32 | Yes | |
 fmaf64 | Yes | |
 fmul_fast | Partial | [#809](https://github.com/model-checking/kani/issues/809) |
-forget | Partial | Generates `SKIP` statement |
+forget | Yes | |
 frem_fast | No | |
 fsub_fast | Yes | |
 likely | Yes | |

tests/kani/Intrinsics/Forget/forget_fail.rs

@@ -0,0 +1,22 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-check-fail
+
+// Checks that `forget` produces a compilation error if the value is referenced
+// after "forgetting" it
+
+// This test is a modified version of the code found in
+// https://doc.rust-lang.org/std/mem/fn.forget.html#relationship-with-manuallydrop
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+ let mut v = vec![65, 122];
+ // Build a `String` using the contents of `v`
+ let s = unsafe { String::from_raw_parts(v.as_mut_ptr(), v.len(), v.capacity()) };
+ // leak `v` because its memory is now managed by `s`
+ std::intrinsics::forget(v); // v is now invalid and must not be passed to a function
+ assert!(v[0] == 65); // Error: v is referenced after `forget`
+ assert_eq!(s, "Az");
+ // `s` is implicitly dropped and its memory deallocated.
+}

tests/kani/Intrinsics/Forget/forget_ok.rs

@@ -0,0 +1,20 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `forget` does not cause a compilation error if the value is not
+// referenced after "forgetting" it
+
+// This test is a modified version of the code found in
+// https://doc.rust-lang.org/std/mem/fn.forget.html#relationship-with-manuallydrop
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+ let mut v = vec![65, 122];
+ // Build a `String` using the contents of `v`
+ let s = unsafe { String::from_raw_parts(v.as_mut_ptr(), v.len(), v.capacity()) };
+ // leak `v` because its memory is now managed by `s`
+ std::intrinsics::forget(v); // v is now invalid and must not be passed to a function
+ assert_eq!(s, "Az");
+ // `s` is implicitly dropped and its memory deallocated.
+}