From a0030c559af8bb926c558564c439c77b87324b41 Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Thu, 13 Nov 2025 21:33:35 -0800 Subject: [PATCH 01/17] Initial commit --- crates/flux-bin/src/lib.rs | 6 ++++++ crates/flux-config/src/flags.rs | 2 +- crates/flux-config/src/lib.rs | 4 ++++ crates/flux-refineck/src/checker.rs | 2 +- 4 files changed, 12 insertions(+), 2 deletions(-) diff --git a/crates/flux-bin/src/lib.rs b/crates/flux-bin/src/lib.rs index 05bcf6b75f2..3ef955a09ba 100644 --- a/crates/flux-bin/src/lib.rs +++ b/crates/flux-bin/src/lib.rs @@ -29,6 +29,9 @@ pub struct FluxMetadata { /// If present, only check files that match any of the glob patterns. Patterns are checked /// relative to the location of the manifest file. pub include: Option>, + /// If present, every function in the module is implicitly labeled with a `no_panic` by default. + /// This means that the only way a function can panic is (1) if it panics, or (2) it calls an external function without this attribute. + pub no_panic: Option, } impl FluxMetadata { @@ -52,6 +55,9 @@ impl FluxMetadata { if let Some(v) = self.default_trusted { flags.push(format!("-Ftrusted={v}")); } + if let Some(v) = self.no_panic { + flags.push(format!("-Fno-panic={v}")); + } if let Some(v) = self.default_ignore { flags.push(format!("-Fignore={v}")); } diff --git a/crates/flux-config/src/flags.rs b/crates/flux-config/src/flags.rs index 43648127cc7..24cfddd8232 100644 --- a/crates/flux-config/src/flags.rs +++ b/crates/flux-config/src/flags.rs @@ -125,7 +125,7 @@ pub(crate) static FLAGS: LazyLock = LazyLock::new(|| { "trusted" => parse_bool(&mut flags.trusted_default, value), "ignore" => parse_bool(&mut flags.ignore_default, value), "emit_lean_defs" => parse_bool(&mut flags.emit_lean_defs, value), - "no_panic" => parse_bool(&mut flags.no_panic, value), + "no-panic" => parse_bool(&mut flags.no_panic, value), _ => { eprintln!("error: unknown flux option: `{key}`"); process::exit(EXIT_FAILURE); diff --git a/crates/flux-config/src/lib.rs b/crates/flux-config/src/lib.rs index 274666f99ba..9a5a47a7f1a 100644 --- a/crates/flux-config/src/lib.rs +++ b/crates/flux-config/src/lib.rs @@ -82,6 +82,10 @@ fn scrape_quals() -> bool { FLAGS.scrape_quals } +pub fn no_panic() -> bool { + FLAGS.no_panic +} + pub fn smt_define_fun() -> bool { FLAGS.smt_define_fun } diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 4159a95bba3..828701c7830 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -877,7 +877,7 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { let tcx = genv.tcx(); if M::NAME == "refine" { - let no_panic = genv.no_panic(self.checker_id.root_id()); + let no_panic = genv.no_panic(self.checker_id.root_id()) || config::no_panic(); if no_panic && let Some(callee_def_id) = callee_def_id From 9aa204b6b52ab98b9e1bdea365473764bb1f8a5b Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Thu, 13 Nov 2025 21:49:01 -0800 Subject: [PATCH 02/17] Update PanicError message to be more helpful --- crates/flux-refineck/locales/en-US.ftl | 2 +- crates/flux-refineck/src/checker.rs | 4 +++- tests/tests/neg/surface/no_panic00.rs | 2 +- 3 files changed, 5 insertions(+), 3 deletions(-) diff --git a/crates/flux-refineck/locales/en-US.ftl b/crates/flux-refineck/locales/en-US.ftl index 0cb24b5bfd7..7cad332d5ce 100644 --- a/crates/flux-refineck/locales/en-US.ftl +++ b/crates/flux-refineck/locales/en-US.ftl @@ -16,7 +16,7 @@ refineck_refine_error = .label = a {$cond} cannot be proved refineck_panic_error = - call to function that may panic + call to {$callee} may panic refineck_div_error = possible division by zero diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 828701c7830..8fab7f769be 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -885,7 +885,8 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { { let callee_no_panic = genv.no_panic(callee_def_id); if !callee_no_panic { - genv.sess().emit_err(errors::PanicError { span }); + let callee_name = tcx.def_path_str(callee_def_id); + genv.sess().emit_err(errors::PanicError { span, callee: callee_name }); } } } @@ -2233,6 +2234,7 @@ pub(crate) mod errors { pub(super) struct PanicError { #[primary_span] pub(super) span: Span, + pub(super) callee: String, } #[derive(Debug)] diff --git a/tests/tests/neg/surface/no_panic00.rs b/tests/tests/neg/surface/no_panic00.rs index 8a101afbee6..8e620cfa8d9 100644 --- a/tests/tests/neg/surface/no_panic00.rs +++ b/tests/tests/neg/surface/no_panic00.rs @@ -1,6 +1,6 @@ #[flux::no_panic] fn calls_unsafe() { - wildcard(); //~ ERROR call to function that may panic + wildcard(); //~ ERROR may panic } From 5252ce8ea3ebc94c2c4996c842196a78341f91ab Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Fri, 14 Nov 2025 13:28:18 -0800 Subject: [PATCH 03/17] Initial try at adding parent traversal --- crates/flux-middle/src/queries.rs | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/crates/flux-middle/src/queries.rs b/crates/flux-middle/src/queries.rs index ca1dd636d6f..c8710d9ec2c 100644 --- a/crates/flux-middle/src/queries.rs +++ b/crates/flux-middle/src/queries.rs @@ -594,9 +594,27 @@ impl<'genv, 'tcx> Queries<'genv, 'tcx> { MaybeExternId::Local(def_id) => def_id, MaybeExternId::Extern(def_id, _) => def_id, }; - genv.fhir_attr_map(local_id).no_panic() + + // 1. First, check to see if this item has the `no_panic` attribute + if genv.fhir_attr_map(local_id).no_panic() { + return true; + } + + // 2. If not, walk up the parent chain to see if any parent has the attribute + if let Some(parent) = genv.tcx().opt_local_parent(local_id) { + println!("going up to parent {parent:?} from {def_id:?}"); + return genv.no_panic(parent); + } else { + println!("no parent for {def_id:?}"); + } + + false + + }, + |def_id| { + println!("hello from cstore"); + genv.cstore().no_panic(def_id) }, - |def_id| genv.cstore().no_panic(def_id), |_| false, ) }) From fd138e4b0360bccf0b7fba8a6aa0b540430190cd Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Fri, 14 Nov 2025 13:51:18 -0800 Subject: [PATCH 04/17] Remove debug prints --- crates/flux-middle/src/queries.rs | 4 ---- 1 file changed, 4 deletions(-) diff --git a/crates/flux-middle/src/queries.rs b/crates/flux-middle/src/queries.rs index c8710d9ec2c..935d252fa0a 100644 --- a/crates/flux-middle/src/queries.rs +++ b/crates/flux-middle/src/queries.rs @@ -602,17 +602,13 @@ impl<'genv, 'tcx> Queries<'genv, 'tcx> { // 2. If not, walk up the parent chain to see if any parent has the attribute if let Some(parent) = genv.tcx().opt_local_parent(local_id) { - println!("going up to parent {parent:?} from {def_id:?}"); return genv.no_panic(parent); - } else { - println!("no parent for {def_id:?}"); } false }, |def_id| { - println!("hello from cstore"); genv.cstore().no_panic(def_id) }, |_| false, From df667eb7c1db5bb97aeb34911b09838c728876f4 Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Sat, 15 Nov 2025 12:31:55 -0800 Subject: [PATCH 05/17] Ignore dummy items and move up to next parent --- crates/flux-middle/src/queries.rs | 36 ++++++++++++++++++++----------- 1 file changed, 24 insertions(+), 12 deletions(-) diff --git a/crates/flux-middle/src/queries.rs b/crates/flux-middle/src/queries.rs index 935d252fa0a..b2b0703990a 100644 --- a/crates/flux-middle/src/queries.rs +++ b/crates/flux-middle/src/queries.rs @@ -590,27 +590,39 @@ impl<'genv, 'tcx> Queries<'genv, 'tcx> { def_id.dispatch_query( genv, |def_id| { - let local_id = match def_id { + let mut current_id = match def_id { MaybeExternId::Local(def_id) => def_id, MaybeExternId::Extern(def_id, _) => def_id, }; - // 1. First, check to see if this item has the `no_panic` attribute - if genv.fhir_attr_map(local_id).no_panic() { - return true; - } + // Walk up the entire parent chain within this closure + loop { + // Skip dummy items + if genv.is_dummy(current_id) { + if let Some(parent) = genv.tcx().opt_local_parent(current_id) { + current_id = parent; + continue; + } else { + return false; // Reached top without finding non-dummy + } + } + + // Check if current non-dummy item has the `no_panic` attribute + if genv.fhir_attr_map(current_id).no_panic() { + return true; + } - // 2. If not, walk up the parent chain to see if any parent has the attribute - if let Some(parent) = genv.tcx().opt_local_parent(local_id) { - return genv.no_panic(parent); + // Move to the next parent + if let Some(parent) = genv.tcx().opt_local_parent(current_id) { + current_id = parent; + } else { + break; // Reached the top + } } false - - }, - |def_id| { - genv.cstore().no_panic(def_id) }, + |def_id| genv.cstore().no_panic(def_id), |_| false, ) }) From 9e9672cd42e4decb8074572eef0d46b805169521 Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Sat, 15 Nov 2025 12:33:01 -0800 Subject: [PATCH 06/17] No panic module-level tests --- tests/tests/neg/surface/no_panic01.rs | 19 +++++++++++++++++++ tests/tests/pos/surface/no_panic02.rs | 13 +++++++++++++ 2 files changed, 32 insertions(+) create mode 100644 tests/tests/neg/surface/no_panic01.rs create mode 100644 tests/tests/pos/surface/no_panic02.rs diff --git a/tests/tests/neg/surface/no_panic01.rs b/tests/tests/neg/surface/no_panic01.rs new file mode 100644 index 00000000000..01b075f831c --- /dev/null +++ b/tests/tests/neg/surface/no_panic01.rs @@ -0,0 +1,19 @@ +pub fn this_might_panic() -> i32 { + let v = vec![1, 2, 3]; + v[0] +} + +#[cfg_attr(flux, flux::no_panic)] +mod my_module { + use super::this_might_panic; + trait MyTrait { + fn do_something(&self) -> i32; + } + + struct MyStruct; + impl MyTrait for MyStruct { + fn do_something(&self) -> i32 { + this_might_panic() //~ ERROR may panic + } + } +} diff --git a/tests/tests/pos/surface/no_panic02.rs b/tests/tests/pos/surface/no_panic02.rs new file mode 100644 index 00000000000..dc1e51a09a0 --- /dev/null +++ b/tests/tests/pos/surface/no_panic02.rs @@ -0,0 +1,13 @@ +#[cfg_attr(flux, flux::no_panic)] +mod my_module { + trait MyTrait { + fn do_something(&self) -> i32; + } + + struct MyStruct; + impl MyTrait for MyStruct { + fn do_something(&self) -> i32 { + 42 + } + } +} \ No newline at end of file From ab908d5bdefc289fe82865c619082df762dc3a74 Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Sat, 15 Nov 2025 12:34:57 -0800 Subject: [PATCH 07/17] Another test for no_panic outside current module --- tests/tests/pos/surface/no_panic03.rs | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 tests/tests/pos/surface/no_panic03.rs diff --git a/tests/tests/pos/surface/no_panic03.rs b/tests/tests/pos/surface/no_panic03.rs new file mode 100644 index 00000000000..7fddcd70e03 --- /dev/null +++ b/tests/tests/pos/surface/no_panic03.rs @@ -0,0 +1,19 @@ +#[flux::no_panic] +pub fn this_might_panic() -> i32 { + 3 +} + +#[cfg_attr(flux, flux::no_panic)] +mod my_module { + use super::this_might_panic; + trait MyTrait { + fn do_something(&self) -> i32; + } + + struct MyStruct; + impl MyTrait for MyStruct { + fn do_something(&self) -> i32 { + this_might_panic() //~ ERROR may panic + } + } +} From 9bc11d07153f7198b1d30253a3fe4bd95db22a92 Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Sat, 15 Nov 2025 12:37:31 -0800 Subject: [PATCH 08/17] Fmt --- crates/flux-refineck/src/checker.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 8fab7f769be..9dfec08bfdd 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -886,7 +886,8 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { let callee_no_panic = genv.no_panic(callee_def_id); if !callee_no_panic { let callee_name = tcx.def_path_str(callee_def_id); - genv.sess().emit_err(errors::PanicError { span, callee: callee_name }); + genv.sess() + .emit_err(errors::PanicError { span, callee: callee_name }); } } } From 9858f32661a4929a922ed68ebddc968308cac259 Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Mon, 17 Nov 2025 09:16:15 -0800 Subject: [PATCH 09/17] Update unit test to include inter-module no_panic --- tests/tests/pos/surface/no_panic03.rs | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/tests/tests/pos/surface/no_panic03.rs b/tests/tests/pos/surface/no_panic03.rs index 7fddcd70e03..e8d9f4ddb4e 100644 --- a/tests/tests/pos/surface/no_panic03.rs +++ b/tests/tests/pos/surface/no_panic03.rs @@ -1,11 +1,14 @@ -#[flux::no_panic] -pub fn this_might_panic() -> i32 { - 3 +#[cfg_attr(flux, flux::no_panic)] +mod my_other_module { + pub fn this_wont_panic() -> i32 { + 3 + } } + #[cfg_attr(flux, flux::no_panic)] mod my_module { - use super::this_might_panic; + use super::my_other_module; trait MyTrait { fn do_something(&self) -> i32; } @@ -13,7 +16,7 @@ mod my_module { struct MyStruct; impl MyTrait for MyStruct { fn do_something(&self) -> i32 { - this_might_panic() //~ ERROR may panic + my_other_module::this_wont_panic() } } } From 1ac386f102e3f231015fd8588d4ccf43e49ee516 Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Mon, 17 Nov 2025 09:28:30 -0800 Subject: [PATCH 10/17] len doesn't panic --- lib/flux-core/src/slice/mod.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/lib/flux-core/src/slice/mod.rs b/lib/flux-core/src/slice/mod.rs index 11666dc4018..c692937f473 100644 --- a/lib/flux-core/src/slice/mod.rs +++ b/lib/flux-core/src/slice/mod.rs @@ -5,6 +5,7 @@ use flux_attrs::*; #[extern_spec(core::slice)] impl [T] { + #[no_panic] #[sig(fn(&Self[@n]) -> usize[n])] fn len(&self) -> usize; From e7d8f2a44bf32d969f7b5d9a901a38faf4368b39 Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Mon, 17 Nov 2025 10:26:45 -0800 Subject: [PATCH 11/17] Address Nico comments --- crates/flux-middle/src/queries.rs | 8 +++----- crates/flux-refineck/src/checker.rs | 2 +- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/crates/flux-middle/src/queries.rs b/crates/flux-middle/src/queries.rs index b2b0703990a..0bc734aea8c 100644 --- a/crates/flux-middle/src/queries.rs +++ b/crates/flux-middle/src/queries.rs @@ -6,6 +6,7 @@ use std::{ use flux_arc_interner::List; use flux_common::{bug, tracked_span_bug}; use flux_errors::{E0999, ErrorGuaranteed}; +use flux_config as config; use flux_rustc_bridge::{ self, def_id_to_string, lowering::{self, Lower, UnsupportedErr}, @@ -590,10 +591,7 @@ impl<'genv, 'tcx> Queries<'genv, 'tcx> { def_id.dispatch_query( genv, |def_id| { - let mut current_id = match def_id { - MaybeExternId::Local(def_id) => def_id, - MaybeExternId::Extern(def_id, _) => def_id, - }; + let mut current_id = def_id.local_id(); // Walk up the entire parent chain within this closure loop { @@ -620,7 +618,7 @@ impl<'genv, 'tcx> Queries<'genv, 'tcx> { } } - false + config::no_panic() }, |def_id| genv.cstore().no_panic(def_id), |_| false, diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 9dfec08bfdd..a09054096ea 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -877,7 +877,7 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { let tcx = genv.tcx(); if M::NAME == "refine" { - let no_panic = genv.no_panic(self.checker_id.root_id()) || config::no_panic(); + let no_panic = genv.no_panic(self.checker_id.root_id()); if no_panic && let Some(callee_def_id) = callee_def_id From 940ed0a3f97da90c4a93f484d7f83bd7a3370a20 Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Mon, 17 Nov 2025 10:26:59 -0800 Subject: [PATCH 12/17] Clippy, fmt --- crates/flux-middle/src/queries.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/flux-middle/src/queries.rs b/crates/flux-middle/src/queries.rs index 0bc734aea8c..99db6dfaa6b 100644 --- a/crates/flux-middle/src/queries.rs +++ b/crates/flux-middle/src/queries.rs @@ -5,8 +5,8 @@ use std::{ use flux_arc_interner::List; use flux_common::{bug, tracked_span_bug}; -use flux_errors::{E0999, ErrorGuaranteed}; use flux_config as config; +use flux_errors::{E0999, ErrorGuaranteed}; use flux_rustc_bridge::{ self, def_id_to_string, lowering::{self, Lower, UnsupportedErr}, From 2bd99c60ac9f57635dfadc61183124754f4fa1d2 Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Mon, 17 Nov 2025 10:46:44 -0800 Subject: [PATCH 13/17] Add num module and implement no_panic saturating_sub function; update slice module with no_panic split_at function --- lib/flux-core/src/lib.rs | 3 +++ lib/flux-core/src/num/mod.rs | 9 +++++++++ lib/flux-core/src/slice/mod.rs | 4 ++++ 3 files changed, 16 insertions(+) create mode 100644 lib/flux-core/src/num/mod.rs diff --git a/lib/flux-core/src/lib.rs b/lib/flux-core/src/lib.rs index b1176048d2c..4dc8ac213ad 100644 --- a/lib/flux-core/src/lib.rs +++ b/lib/flux-core/src/lib.rs @@ -17,6 +17,9 @@ mod clone; #[cfg(flux)] mod slice; +#[cfg(flux)] +mod num; + // ------------------------------------------------------------------- #[macro_export] diff --git a/lib/flux-core/src/num/mod.rs b/lib/flux-core/src/num/mod.rs new file mode 100644 index 00000000000..727c213c4c0 --- /dev/null +++ b/lib/flux-core/src/num/mod.rs @@ -0,0 +1,9 @@ + +use flux_attrs::*; + +#[extern_spec(core::num)] +impl usize { + #[no_panic] + fn saturating_sub(self, other: usize) -> usize; + +} \ No newline at end of file diff --git a/lib/flux-core/src/slice/mod.rs b/lib/flux-core/src/slice/mod.rs index c692937f473..68be095ccae 100644 --- a/lib/flux-core/src/slice/mod.rs +++ b/lib/flux-core/src/slice/mod.rs @@ -17,6 +17,10 @@ impl [T] { #[sig(fn(&Self[@n]) -> Iter[0, n])] fn iter(&self) -> Iter<'_, T>; + + #[no_panic] + #[sig(fn(&Self[@n], mid: usize{mid <= n}) -> (&[T][mid], &[T][n - mid]))] + fn split_at(&self, mid: usize) -> (&[T], &[T]); } #[cfg(flux_sysroot_test)] From b509fb8735239929ceda3e67c29b348402c1cf8f Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Mon, 17 Nov 2025 10:49:53 -0800 Subject: [PATCH 14/17] Add no_panic to index --- lib/flux-core/src/slice/index.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/lib/flux-core/src/slice/index.rs b/lib/flux-core/src/slice/index.rs index 05811498e62..a31e9dea7f6 100644 --- a/lib/flux-core/src/slice/index.rs +++ b/lib/flux-core/src/slice/index.rs @@ -11,6 +11,7 @@ impl> ops::Index for [T] { } )] + #[no_panic] #[sig(fn(&Self[@len], {I[@idx] | >::in_bounds(len, idx)}) -> &I::Output)] fn index(&self, index: I) -> &I::Output; } From 208e1b33739411f5a517064851eb1933ae5405bc Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Tue, 18 Nov 2025 14:07:19 -0800 Subject: [PATCH 15/17] Clippy --- lib/flux-core/src/num/mod.rs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/lib/flux-core/src/num/mod.rs b/lib/flux-core/src/num/mod.rs index 727c213c4c0..701d6589322 100644 --- a/lib/flux-core/src/num/mod.rs +++ b/lib/flux-core/src/num/mod.rs @@ -1,9 +1,7 @@ - use flux_attrs::*; #[extern_spec(core::num)] impl usize { #[no_panic] fn saturating_sub(self, other: usize) -> usize; - -} \ No newline at end of file +} From 4cb07485670a85807981d8a70a778bc2785522a3 Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Tue, 18 Nov 2025 14:07:31 -0800 Subject: [PATCH 16/17] Add another unit test --- tests/tests/pos/surface/no_panic04.rs | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 tests/tests/pos/surface/no_panic04.rs diff --git a/tests/tests/pos/surface/no_panic04.rs b/tests/tests/pos/surface/no_panic04.rs new file mode 100644 index 00000000000..ccc387f2a45 --- /dev/null +++ b/tests/tests/pos/surface/no_panic04.rs @@ -0,0 +1,22 @@ +trait MyTrait { + fn f1(&self) -> usize; + fn f2(&self) -> usize; +} + +struct MyImpl {} + +impl MyTrait for MyImpl { + #[flux_rs::no_panic] + fn f1(&self) -> usize { + self.f2() + } + #[flux_rs::no_panic] + fn f2(&self) -> usize { + 2 + } +} + +#[flux_rs::no_panic] +fn test00(x: &MyImpl) -> usize { + x.f1() + x.f2() +} From 1a7c3ce122961f6a2f5f1faaa16b5d0eeb341147 Mon Sep 17 00:00:00 2001 From: Andrew Cheung Date: Tue, 18 Nov 2025 14:10:20 -0800 Subject: [PATCH 17/17] Address Evan comment --- crates/flux-bin/src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/flux-bin/src/lib.rs b/crates/flux-bin/src/lib.rs index 3ef955a09ba..ba1b7ca3958 100644 --- a/crates/flux-bin/src/lib.rs +++ b/crates/flux-bin/src/lib.rs @@ -30,7 +30,7 @@ pub struct FluxMetadata { /// relative to the location of the manifest file. pub include: Option>, /// If present, every function in the module is implicitly labeled with a `no_panic` by default. - /// This means that the only way a function can panic is (1) if it panics, or (2) it calls an external function without this attribute. + /// This means that the only way a function can panic is if it calls an external function without this attribute. pub no_panic: Option, }