Hide --lib-c and add assume-false to unknown fns (rust-lang#964)

 - Support to --lib-c is not well tested. Keep it as experiemental.
 - Change how CBMC behaves when a function that is not defined is
   reachable. This mitigates issues rust-lang#576. We should still add an
   unimplemented assertion so we can flip the results of other checks to
   undetermined.

Author: celinval

src/cargo-kani/src/args.rs

@@ -75,8 +75,9 @@ pub struct KaniArgs {
     /// Entry point for verification
     #[structopt(long, default_value = "main")]
     pub function: String,
-    /// Link external C files referenced by Rust code
-    #[structopt(long, parse(from_os_str))]
+    /// Link external C files referenced by Rust code.
+    /// This is an experimental feature.
+    #[structopt(long, parse(from_os_str), hidden = true)]
     pub c_lib: Vec<PathBuf>,
     /// Enable test function verification. Only use this option when the entry point is a test function.
     #[structopt(long)]

src/cargo-kani/src/call_goto_instrument.rs

@@ -79,7 +79,7 @@ impl KaniSession {
     fn undefined_functions(&self, file: &Path) -> Result<()> {
         let args: Vec<OsString> = vec![
             "--generate-function-body-options".into(),
-            "assert-false".into(),
+            "assert-false-assume-false".into(),
             "--generate-function-body".into(),
             ".*".into(),
             "--drop-unused-functions".into(),

tests/ui/cbmc_checks/float-overflow/check_message.rs

@@ -8,7 +8,7 @@ use kani::any;
 
 // Use the result so rustc doesn't optimize them away.
 fn dummy(result: f32) -> f32 {
-    result.round()
+    result
 }
 
 #[kani::proof]

tests/ui/missing-function/expected

@@ -0,0 +1,5 @@
+Status: UNREACHABLE\
+Description: "assertion failed: x == 5"
+
+VERIFICATION:- FAILED
+

tests/ui/missing-function/extern_c.rs

@@ -0,0 +1,19 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --function harness
+
+// This test is to check Kani's error handling for missing functions.
+// TODO: Verify that this prints a compiler warning:
+//  - https://github.com/model-checking/kani/issues/576
+
+
+extern "C" {
+    fn missing_function() -> u32;
+}
+
+#[kani::proof]
+fn harness() {
+    let x = unsafe { missing_function() };
+    assert!(x == 5);
+}