Add unstable option assume-no-panic

Compute verification results under the assumption that no panic occurs.

Author: tautschnig

kani-compiler/src/args.rs

@@ -37,6 +37,10 @@ pub enum ReachabilityType {
 /// with. Usually stored in and accessible via [`crate::kani_queries::QueryDb`].
 #[derive(Debug, Default, Clone, clap::Parser)]
 pub struct Arguments {
+    /// 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 assume_no_panic: bool,
     /// Option used to disable asserting function contracts.
     #[clap(long)]
     pub no_assert_contracts: bool,

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().assume_no_panic {
+            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

@@ -212,6 +212,11 @@ pub enum CargoKaniSubcommand {
 #[derive(Debug, clap::Args)]
 #[clap(next_help_heading = "Verification Options")]
 pub struct VerificationArgs {
+    /// 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 assume_no_panic: bool,
+
     /// Link external C files referenced by Rust code.
     /// This is an experimental feature and requires `-Z c-ffi` to be used
     #[arg(long, hide = true, num_args(1..))]
@@ -634,6 +639,12 @@ impl ValidateArgs for VerificationArgs {
 
         // check_unstable() calls: for each unstable option, check that the requisite unstable feature is provided.
         let unstable = || -> Result<(), Error> {
+            self.common_args.check_unstable(
+                self.assume_no_panic,
+                "assume-no-panic",
+                UnstableFeature::UnstableOptions,
+            )?;
+
             self.common_args.check_unstable(
                 self.concrete_playback.is_some(),
                 "concrete-playback",

kani-driver/src/call_single_file.rs

@@ -116,6 +116,10 @@ impl KaniSession {
     pub fn kani_compiler_local_flags(&self) -> Vec<KaniArg> {
         let mut flags: Vec<KaniArg> = vec![];
 
+        if self.args.assume_no_panic {
+            flags.push("--assume-no-panic".into());
+        }
+
         if self.args.common_args.debug {
             flags.push("--log-level=debug".into());
         } else if self.args.common_args.verbose {

tests/kani/Panic/assume_no_panic.rs

@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z unstable-options --assume-no-panic
+//! Test that --assume-no-panic works
+
+#[kani::proof]
+fn div0() -> i32 {
+    let x: i32 = kani::any();
+    let y: i32 = kani::any();
+    x / y
+}