Add unstable option prove-safety-only

kani-compiler/src/args.rs

@@ -65,6 +65,10 @@ pub struct Arguments {
     /// Option used for suppressing global ASM error.
     #[clap(long)]
     pub ignore_global_asm: bool,
+    /// Compute verification results under the assumption that no panic occurs.
+    /// This feature is unstable, and it requires `-Z unstable-options` to be used
+    #[clap(long)]
+    pub prove_safety_only: bool,
     /// Option name used to select which reachability analysis to perform.
     #[clap(long = "reachability", default_value = "none")]
     pub reachability_analysis: ReachabilityType,

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

@@ -133,11 +133,18 @@ impl GotocCtx<'_> {
         message: &str,
         loc: Location,
     ) -> Stmt {
-        let property_name = property_class.as_str();
-        Stmt::block(
-            vec![Stmt::assert(cond.clone(), property_name, message, loc), Stmt::assume(cond, loc)],
-            loc,
-        )
+        if property_class == PropertyClass::Assertion && self.queries.args().prove_safety_only {
+            Stmt::assume(cond, loc)
+        } else {
+            let property_name = property_class.as_str();
+            Stmt::block(
+                vec![
+                    Stmt::assert(cond.clone(), property_name, message, loc),
+                    Stmt::assume(cond, loc),
+                ],
+                loc,
+            )
+        }
     }
 
     /// Generate code to cover the given condition at the current location

kani-driver/src/args/mod.rs

@@ -330,6 +330,11 @@ pub struct VerificationArgs {
     #[arg(long, hide = true)]
     pub print_llbc: bool,
 
+    /// Compute verification results under the assumption that no panic occurs.
+    /// This feature is unstable, and it requires `-Z unstable-options` to be used
+    #[arg(long, hide_short_help = true)]
+    pub prove_safety_only: bool,
+
     /// Randomize the layout of structures. This option can help catching code that relies on
     /// a specific layout chosen by the compiler that is not guaranteed to be stable in the future.
     /// If a value is given, it will be used as the seed for randomization
@@ -726,6 +731,12 @@ impl ValidateArgs for VerificationArgs {
                 UnstableFeature::FunctionContracts,
             )?;
 
+            self.common_args.check_unstable(
+                self.prove_safety_only,
+                "prove-safety-only",
+                UnstableFeature::UnstableOptions,
+            )?;
+
             Ok(())
         };
 

kani-driver/src/call_single_file.rs

@@ -175,6 +175,10 @@ impl KaniSession {
             flags.extend(args.into_iter().map(KaniArg::from));
         }
 
+        if self.args.prove_safety_only {
+            flags.push("--prove-safety-only".into());
+        }
+
         flags.extend(self.args.common_args.unstable_features.as_arguments().map(KaniArg::from));
 
         flags

tests/kani/Panic/prove_safety_only.rs

@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z unstable-options --prove-safety-only
+//! Test that --prove-safety-only works
+
+#[kani::proof]
+fn div0() -> i32 {
+    let x: i32 = kani::any();
+    let y: i32 = kani::any();
+    x / y
+}
+
+#[kani::proof]
+fn assert_hides_ub() {
+    let arr: [u8; 5] = kani::any();
+    let mut bytes = kani::slice::any_slice_of_array(&arr);
+    let slice_offset = unsafe { bytes.as_ptr().offset_from(&arr as *const u8) };
+    let offset: usize = kani::any();
+    assert!(offset <= 4 && (slice_offset as usize) + offset <= 4);
+    let _ = unsafe { *bytes.as_ptr().add(offset) };
+}