Only compile as binary target if verifying main function (rust-lang#869)

* Only compile as binary target if verifying main function

In order to verify a harness using `kani` command, user either have to
have a `main` function defined in their crate or they have to set the
env variable RUSTFLAGS to include --crate-type lib.

With these changes, Kani will pick the crate type based on the
--function argument.

* Update call_single_file.rs

Author: celinval

src/cargo-kani/src/call_single_file.rs

@@ -54,6 +54,15 @@ impl KaniSession {
             if !args.contains(&t) {
                 args.push(t);
             }
+        } else {
+            if self.args.function != "main" {
+                // Unless entry function for proof harness is main, compile code as lib.
+                // This ensures that rustc won't prune functions that are not reachable
+                // from main as well as enable compilation of crates that don't have a main
+                // function.
+                args.push("--crate-type".into());
+                args.push("lib".into());
+            }
         }
 
         let mut cmd = Command::new(&self.kani_rustc);

tests/expected/reach/unreachable/expected

@@ -1,2 +1,2 @@
 UNREACHABLE
- ** 1 of 5 failed (1 unreachable)
+ ** 1 of 3 failed (1 unreachable)

tests/expected/reach/unreachable/test.rs

@@ -16,5 +16,3 @@ fn foo(x: i32) {
         assert!(x <= 5);
     }
 }
-
-fn main() {}