diff --git a/charon/Cargo.lock b/charon/Cargo.lock index d489faf4e..643c65125 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -807,7 +807,7 @@ checksum = "9229cfe53dfd69f0609a49f65461bd93001ea1ef889cd5529dd176593f5338a1" [[package]] name = "hax-adt-into" version = "0.3.1" -source = "git+https://github.com/AeneasVerif/hax?branch=main#24991a867cb5886f3c9ddad7a9ca0ad03b80c629" +source = "git+https://github.com/AeneasVerif/hax?branch=main#0c442212e193e6d058c46a1960f8dc8505dd38fa" dependencies = [ "itertools 0.11.0", "proc-macro2", @@ -818,7 +818,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter" version = "0.3.1" -source = "git+https://github.com/AeneasVerif/hax?branch=main#24991a867cb5886f3c9ddad7a9ca0ad03b80c629" +source = "git+https://github.com/AeneasVerif/hax?branch=main#0c442212e193e6d058c46a1960f8dc8505dd38fa" dependencies = [ "extension-traits", "hax-adt-into", @@ -835,7 +835,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter-options" version = "0.3.1" -source = "git+https://github.com/AeneasVerif/hax?branch=main#24991a867cb5886f3c9ddad7a9ca0ad03b80c629" +source = "git+https://github.com/AeneasVerif/hax?branch=main#0c442212e193e6d058c46a1960f8dc8505dd38fa" dependencies = [ "hax-adt-into", "schemars", diff --git a/charon/src/bin/charon-driver/translate/translate_crate.rs b/charon/src/bin/charon-driver/translate/translate_crate.rs index 9069a2c1f..0f9119041 100644 --- a/charon/src/bin/charon-driver/translate/translate_crate.rs +++ b/charon/src/bin/charon-driver/translate/translate_crate.rs @@ -245,12 +245,16 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { let Some(kind) = self.base_kind_for_item(def_id) else { return; }; - let item_src = if self.options.monomorphize_with_hax - && let Ok(def) = self.poly_hax_def(def_id) - && !def.has_any_generics() - { - // Monomorphize this item and the items it depends on. - TransItemSource::monomorphic(def.this(), kind) + let item_src = if self.options.monomorphize_with_hax { + if let Ok(def) = self.poly_hax_def(def_id) + && !def.has_any_generics() + { + // Monomorphize this item and the items it depends on. + TransItemSource::monomorphic(def.this(), kind) + } else { + // Skip polymorphic items and items that cause errors. + return; + } } else { TransItemSource::polymorphic(def_id, kind) }; diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index a1a433489..12226a1d8 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -133,7 +133,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { let def_id = item.def_id(); let span = self.def_span(def_id); if let RustcItem::Mono(item_ref) = item - && item_ref.has_param + && item_ref.has_non_lt_param { raise_error!(self, span, "Item is not monomorphic: {item:?}") } diff --git a/charon/src/bin/charon-driver/translate/translate_items.rs b/charon/src/bin/charon-driver/translate/translate_items.rs index 76e86cc87..d4b10e92b 100644 --- a/charon/src/bin/charon-driver/translate/translate_items.rs +++ b/charon/src/bin/charon-driver/translate/translate_items.rs @@ -680,6 +680,8 @@ impl ItemTransCtx<'_, '_> { let ty = self.translate_ty(item_span, ty)?; consts.push((item_name.clone(), ty)); } + // Monomorphic traits have no associated types. + hax::FullDefKind::AssocTy { .. } if self.monomorphize() => continue, hax::FullDefKind::AssocTy { param_env, .. } if !param_env.generics.params.is_empty() => { @@ -890,6 +892,8 @@ impl ItemTransCtx<'_, '_> { }; consts.push((name, gref)); } + // Monomorphic traits have no associated types. + hax::FullDefKind::AssocTy { .. } if self.monomorphize() => continue, hax::FullDefKind::AssocTy { param_env, .. } if !param_env.generics.params.is_empty() => { @@ -1057,17 +1061,20 @@ impl ItemTransCtx<'_, '_> { let mut types = vec![]; let mut type_clauses = vec![]; - let type_items = trait_items.iter().filter(|assoc| match assoc.kind { - hax::AssocKind::Type { .. } => true, - _ => false, - }); - for ((ty, impl_exprs), assoc) in vimpl.types.iter().zip(type_items) { - let name = self.t_ctx.translate_trait_item_name(&assoc.def_id)?; - let ty = self.translate_ty(span, ty)?; - types.push((name.clone(), ty.clone())); - if !self.monomorphize() { - let trait_refs = self.translate_trait_impl_exprs(span, impl_exprs)?; - type_clauses.push((name.clone(), trait_refs)); + // Monomorphic traits have no associated types. + if !self.monomorphize() { + let type_items = trait_items.iter().filter(|assoc| match assoc.kind { + hax::AssocKind::Type { .. } => true, + _ => false, + }); + for ((ty, impl_exprs), assoc) in vimpl.types.iter().zip(type_items) { + let name = self.t_ctx.translate_trait_item_name(&assoc.def_id)?; + let ty = self.translate_ty(span, ty)?; + types.push((name.clone(), ty.clone())); + if !self.monomorphize() { + let trait_refs = self.translate_trait_impl_exprs(span, impl_exprs)?; + type_clauses.push((name.clone(), trait_refs)); + } } } diff --git a/charon/src/errors.rs b/charon/src/errors.rs index f191d5a93..dd7b07bd0 100644 --- a/charon/src/errors.rs +++ b/charon/src/errors.rs @@ -10,6 +10,8 @@ use petgraph::prelude::DiGraphMap; use std::cmp::{Ord, PartialOrd}; use std::collections::{HashMap, HashSet}; +const BACKTRACE_ON_ERR: bool = false; + #[macro_export] macro_rules! register_error { ($ctx:expr, crate($krate:expr), $span: expr, $($fmt:tt)*) => {{ @@ -231,6 +233,10 @@ impl ErrorCtx { ) -> Error { let error = Error { span, msg }; anstream::eprintln!("{}\n", error.render(krate, level)); + if BACKTRACE_ON_ERR { + let backtrace = std::backtrace::Backtrace::force_capture(); + eprintln!("{backtrace}\n"); + } error } diff --git a/charon/tests/ui/dyn-with-diamond-supertraits.out b/charon/tests/ui/dyn-with-diamond-supertraits.out new file mode 100644 index 000000000..5e596cc2d --- /dev/null +++ b/charon/tests/ui/dyn-with-diamond-supertraits.out @@ -0,0 +1,11 @@ + +thread 'rustc' panicked at src/bin/charon-driver/translate/translate_trait_objects.rs:426:14: +trait should be dyn-compatible +note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace +error: Thread panicked when extracting item `test_crate::{impl#4}`. + --> tests/ui/dyn-with-diamond-supertraits.rs:47:1 + | +47 | impl Join for i32 { + | ^^^^^^^^^^^^^^^^^^^^^^ + +ERROR Charon failed to translate this code (1 errors) diff --git a/charon/tests/ui/dyn-with-diamond-supertraits.rs b/charon/tests/ui/dyn-with-diamond-supertraits.rs new file mode 100644 index 000000000..67e845c74 --- /dev/null +++ b/charon/tests/ui/dyn-with-diamond-supertraits.rs @@ -0,0 +1,56 @@ +//@ known-failure +/// This tests `dyn` with a diamond hierarchy between supertraits. Fails for now because we don't +/// support dyn with associated types. + +trait Super { + fn super_method(&self, arg: T) -> i32; +} +trait Internal { + type Internal; + fn internal_method(&self) -> Self::Internal; +} +trait Left: Internal { + type Left; + fn left_method(&self) -> Self::Left; +} +trait Right: Internal + Super { + type Right; + fn right_method(&self) -> Self::Right; +} +trait Join: Left + Right { + fn join_method(&self) -> (Self::Left, Self::Right); +} + +impl Super for i32 { + fn super_method(&self, arg: i32) -> i32 { + self + arg + } +} +impl Internal for i32 { + type Internal = i32; + fn internal_method(&self) -> Self::Internal { + *self + 1 + } +} +impl Left for i32 { + type Left = i32; + fn left_method(&self) -> Self::Left { + *self + 2 + } +} +impl Right for i32 { + type Right = i32; + fn right_method(&self) -> Self::Right { + *self + 3 + self.internal_method() + self.super_method(10) + } +} +impl Join for i32 { + fn join_method(&self) -> (Self::Left, Self::Right) { + (self.left_method(), self.right_method()) + } +} + +fn main() { + let v: &dyn Join = &97; + let (_, _) = v.join_method(); +} diff --git a/charon/tests/ui/monomorphization/bound_lifetime.out b/charon/tests/ui/monomorphization/bound_lifetime.out new file mode 100644 index 000000000..64fc21d03 --- /dev/null +++ b/charon/tests/ui/monomorphization/bound_lifetime.out @@ -0,0 +1,63 @@ +# Final LLBC before serialization: + +// Full name: core::marker::MetaSized::<&'_ (u32)> +#[lang_item("meta_sized")] +pub trait MetaSized::<&'_ (u32)> + +// Full name: core::marker::Sized::<&'_ (u32)> +#[lang_item("sized")] +pub trait Sized::<&'_ (u32)> +{ + parent_clause0 : [@TraitClause0]: MetaSized::<&'_ (u32)> + non-dyn-compatible +} + +// Full name: core::option::Option::<&'_ (u32)> +#[lang_item("Option")] +pub enum Option::<&'_ (u32)> { + None, + Some(&'_ (u32)), +} + +// Full name: test_crate::foo +fn foo<'_0>(@1: &'_0 (u32)) -> Option::<&'_ (u32)> +{ + let @0: Option::<&'_ (u32)>; // return + let x@1: &'_ (u32); // arg #1 + let @2: &'_ (u32); // anonymous local + + storage_live(@2) + @2 := &*(x@1) + @0 := Option::<&'_ (u32)>::Some { 0: move (@2) } + storage_dead(@2) + return +} + +// Full name: test_crate::main +fn main() +{ + let @0: (); // return + let @1: Option::<&'_ (u32)>; // anonymous local + let @2: &'_ (u32); // anonymous local + let @3: &'_ (u32); // anonymous local + let @4: u32; // anonymous local + + storage_live(@1) + storage_live(@2) + storage_live(@3) + storage_live(@4) + @4 := const (42 : u32) + @3 := &@4 + @2 := &*(@3) + @1 := foo<'_>(move (@2)) + storage_dead(@2) + storage_dead(@4) + storage_dead(@3) + storage_dead(@1) + @0 := () + @0 := () + return +} + + + diff --git a/charon/tests/ui/monomorphization/bound_lifetime.rs b/charon/tests/ui/monomorphization/bound_lifetime.rs new file mode 100644 index 000000000..d2a5ae602 --- /dev/null +++ b/charon/tests/ui/monomorphization/bound_lifetime.rs @@ -0,0 +1,9 @@ +//@ charon-args=--monomorphize +/// Reproducer for a bug whereby a bound lifetime was not allowed in monomorphic context. +fn foo(x: &u32) -> Option<&u32> { + Some(x) +} + +fn main() { + let _ = foo(&42); +} diff --git a/charon/tests/ui/monomorphization/closure-fn.out b/charon/tests/ui/monomorphization/closure-fn.out index 693f8591a..1f23a513d 100644 --- a/charon/tests/ui/monomorphization/closure-fn.out +++ b/charon/tests/ui/monomorphization/closure-fn.out @@ -57,7 +57,6 @@ pub trait FnOnce::, (u8, u8)> parent_clause0 : [@TraitClause0]: MetaSized::> parent_clause1 : [@TraitClause1]: Sized::<(u8, u8)> parent_clause2 : [@TraitClause2]: Tuple::<(u8, u8)> - type Output fn call_once = core::ops::function::FnOnce::call_once::, (u8, u8)> non-dyn-compatible } @@ -311,7 +310,6 @@ impl<'_0, '_1> FnOnce::, (u8, u8)> { parent_clause0 = MetaSized::> parent_clause1 = Sized::<(u8, u8)> parent_clause2 = Tuple::<(u8, u8)> - type Output = u8 fn call_once = {impl FnOnce::, (u8, u8)>}::call_once<'_0, '_1> non-dyn-compatible } diff --git a/charon/tests/ui/monomorphization/closure-fnonce.out b/charon/tests/ui/monomorphization/closure-fnonce.out index 2a988b054..6e81c6444 100644 --- a/charon/tests/ui/monomorphization/closure-fnonce.out +++ b/charon/tests/ui/monomorphization/closure-fnonce.out @@ -73,7 +73,6 @@ pub trait FnOnce:: parent_clause0 : [@TraitClause0]: MetaSized:: parent_clause1 : [@TraitClause1]: Sized::<(u8)> parent_clause2 : [@TraitClause2]: Tuple::<(u8)> - type Output fn call_once = core::ops::function::FnOnce::call_once:: non-dyn-compatible } @@ -157,7 +156,6 @@ impl FnOnce:: { parent_clause0 = MetaSized:: parent_clause1 = Sized::<(u8)> parent_clause2 = Tuple::<(u8)> - type Output = u8 fn call_once = {impl FnOnce::}::call_once non-dyn-compatible } diff --git a/charon/tests/ui/monomorphization/closures.out b/charon/tests/ui/monomorphization/closures.out index ea6b79079..9bca2fa34 100644 --- a/charon/tests/ui/monomorphization/closures.out +++ b/charon/tests/ui/monomorphization/closures.out @@ -126,7 +126,6 @@ pub trait FnOnce::, (u8)> parent_clause0 : [@TraitClause0]: MetaSized::> parent_clause1 : [@TraitClause1]: Sized::<(u8)> parent_clause2 : [@TraitClause2]: Tuple::<(u8)> - type Output fn call_once = core::ops::function::FnOnce::call_once::, (u8)> non-dyn-compatible } @@ -166,7 +165,6 @@ pub trait FnOnce::, (u8)> parent_clause0 : [@TraitClause0]: MetaSized::> parent_clause1 : [@TraitClause1]: Sized::<(u8)> parent_clause2 : [@TraitClause2]: Tuple::<(u8)> - type Output fn call_once = core::ops::function::FnOnce::call_once::, (u8)> non-dyn-compatible } @@ -198,7 +196,6 @@ pub trait FnOnce:: parent_clause0 : [@TraitClause0]: MetaSized:: parent_clause1 : [@TraitClause1]: Sized::<(u8)> parent_clause2 : [@TraitClause2]: Tuple::<(u8)> - type Output fn call_once = core::ops::function::FnOnce::call_once:: non-dyn-compatible } @@ -439,7 +436,6 @@ impl<'_0> FnOnce::, (u8)> { parent_clause0 = MetaSized::> parent_clause1 = Sized::<(u8)> parent_clause2 = Tuple::<(u8)> - type Output = u8 fn call_once = {impl FnOnce::, (u8)>}::call_once<'_0> non-dyn-compatible } @@ -484,7 +480,6 @@ impl<'_0> FnOnce::, (u8)> { parent_clause0 = MetaSized::> parent_clause1 = Sized::<(u8)> parent_clause2 = Tuple::<(u8)> - type Output = u8 fn call_once = {impl FnOnce::, (u8)>}::call_once<'_0> non-dyn-compatible } @@ -504,7 +499,6 @@ impl FnOnce:: { parent_clause0 = MetaSized:: parent_clause1 = Sized::<(u8)> parent_clause2 = Tuple::<(u8)> - type Output = u8 fn call_once = {impl FnOnce::}::call_once non-dyn-compatible } diff --git a/charon/tests/ui/monomorphization/closures.rs b/charon/tests/ui/monomorphization/closures.rs index 2be502b60..614f0834f 100644 --- a/charon/tests/ui/monomorphization/closures.rs +++ b/charon/tests/ui/monomorphization/closures.rs @@ -1,5 +1,6 @@ //@ charon-args=--monomorphize //@ charon-args=--start-from=crate::main +//@ charon-args=--remove-associated-types * // Ensures closures are monomorphized and replaced with static function calls struct Thing; diff --git a/charon/tests/ui/monomorphization/dyn-trait.out b/charon/tests/ui/monomorphization/dyn-trait.out index 4119e8c4e..b5c91c4bb 100644 --- a/charon/tests/ui/monomorphization/dyn-trait.out +++ b/charon/tests/ui/monomorphization/dyn-trait.out @@ -55,22 +55,6 @@ note: the error occurred when translating `core::fmt::Display:: /rustc/library/core/src/fmt/mod.rs:562:1 - -note: the error occurred when translating `core::fmt::Display::fmt::`, which is (transitively) used at the following location(s): - --> tests/ui/monomorphization/dyn-trait.rs:11:23 - | -11 | let str: String = "hello".to_string(); - | ------------------- -error: Item is not monomorphic: Mono(ItemRef { contents: Node { id: Id { id: 498 }, value: ItemRefContents { def_id: core::fmt::Formatter, generic_args: [Lifetime(Region { kind: ReBound(0, BoundRegion { var: 2, kind: Anon }) })], impl_exprs: [], in_trait: None, has_param: true } } }) - --> /rustc/library/core/src/fmt/mod.rs:562:1 - -note: the error occurred when translating `core::fmt::Display::fmt::`, which is (transitively) used at the following location(s): - --> tests/ui/monomorphization/dyn-trait.rs:12:27 - | -12 | let _ = dyn_to_string(&str); - | ---- error: `dyn Trait` is not yet supported with `--monomorphize`; use `--monomorphize-conservative` instead --> /rustc/library/core/src/fmt/mod.rs:1028:5 @@ -82,25 +66,6 @@ note: the error occurred when translating `core::fmt::Display::fmt:: /rustc/library/core/src/fmt/mod.rs:1028:5 -error: Item is not monomorphic: Mono(ItemRef { contents: Node { id: Id { id: 498 }, value: ItemRefContents { def_id: core::fmt::Formatter, generic_args: [Lifetime(Region { kind: ReBound(0, BoundRegion { var: 2, kind: Anon }) })], impl_exprs: [], in_trait: None, has_param: true } } }) - --> /rustc/library/core/src/fmt/mod.rs:562:1 - -error: Item is not monomorphic: Mono(ItemRef { contents: Node { id: Id { id: 598 }, value: ItemRefContents { def_id: core::fmt::Formatter, generic_args: [Lifetime(Region { kind: ReBound(0, BoundRegion { var: 2, kind: Anon }) })], impl_exprs: [], in_trait: None, has_param: true } } }) - --> /rustc/library/core/src/fmt/mod.rs:562:1 - -note: the error occurred when translating `core::fmt::{impl core::fmt::Display::}::fmt`, which is (transitively) used at the following location(s): - --> tests/ui/monomorphization/dyn-trait.rs:11:23 - | -11 | let str: String = "hello".to_string(); - | ------------------- -error: Item is not monomorphic: Mono(ItemRef { contents: Node { id: Id { id: 498 }, value: ItemRefContents { def_id: core::fmt::Formatter, generic_args: [Lifetime(Region { kind: ReBound(0, BoundRegion { var: 2, kind: Anon }) })], impl_exprs: [], in_trait: None, has_param: true } } }) - --> /rustc/library/core/src/fmt/mod.rs:562:1 - -note: the error occurred when translating `core::fmt::Display::fmt`, which is (transitively) used at the following location(s): - --> tests/ui/monomorphization/dyn-trait.rs:11:23 - | -11 | let str: String = "hello".to_string(); - | ------------------- error: `dyn Trait` is not yet supported with `--monomorphize`; use `--monomorphize-conservative` instead --> /rustc/library/core/src/marker.rs:179:1 @@ -131,9 +96,6 @@ note: the error occurred when translating `core::fmt::Display::{vtable}:: /rustc/library/core/src/fmt/mod.rs:562:1 - thread 'rustc' panicked at src/bin/charon-driver/translate/translate_trait_objects.rs:375:14: incorrect `dyn_self` @@ -152,22 +114,6 @@ note: the error occurred when translating `alloc::string::{impl core::fmt::Displ error: Item `alloc::string::{impl#23}` caused errors; ignoring. --> /rustc/library/alloc/src/string.rs:2623:1 -error: Item is not monomorphic: Mono(ItemRef { contents: Node { id: Id { id: 671 }, value: ItemRefContents { def_id: core::fmt::Formatter, generic_args: [Lifetime(Region { kind: ReBound(0, BoundRegion { var: 2, kind: Anon }) })], impl_exprs: [], in_trait: None, has_param: true } } }) - --> /rustc/library/core/src/fmt/mod.rs:562:1 - -note: the error occurred when translating `alloc::string::{impl core::fmt::Display::}::fmt`, which is (transitively) used at the following location(s): - --> tests/ui/monomorphization/dyn-trait.rs:12:27 - | -12 | let _ = dyn_to_string(&str); - | ---- -error: Item is not monomorphic: Mono(ItemRef { contents: Node { id: Id { id: 498 }, value: ItemRefContents { def_id: core::fmt::Formatter, generic_args: [Lifetime(Region { kind: ReBound(0, BoundRegion { var: 2, kind: Anon }) })], impl_exprs: [], in_trait: None, has_param: true } } }) - --> /rustc/library/core/src/fmt/mod.rs:562:1 - -note: the error occurred when translating `core::fmt::Display::fmt`, which is (transitively) used at the following location(s): - --> tests/ui/monomorphization/dyn-trait.rs:12:27 - | -12 | let _ = dyn_to_string(&str); - | ---- error: `dyn Trait` is not yet supported with `--monomorphize`; use `--monomorphize-conservative` instead --> /rustc/library/alloc/src/string.rs:2780:1 @@ -252,4 +198,4 @@ note: the error occurred when translating `alloc::string::ToString::to_string`, | 7 | x.to_string() | ------------- -ERROR Charon failed to translate this code (46 errors) +ERROR Charon failed to translate this code (38 errors) diff --git a/charon/tests/ui/monomorphization/fndefs-casts.out b/charon/tests/ui/monomorphization/fndefs-casts.out index 796715336..f5092c8d9 100644 --- a/charon/tests/ui/monomorphization/fndefs-casts.out +++ b/charon/tests/ui/monomorphization/fndefs-casts.out @@ -110,7 +110,6 @@ pub trait FnOnce:: foo::<'_0_0>, (&'_ (u32))> parent_clause0 : [@TraitClause0]: MetaSized:: foo::<'_0_0>> parent_clause1 : [@TraitClause1]: Sized::<(&'_ (u32))> parent_clause2 : [@TraitClause2]: Tuple::<(&'_ (u32))> - type Output fn call_once = call_once:: foo::<'_0_0>, (&'_ (u32))> non-dyn-compatible } diff --git a/charon/tests/ui/monomorphization/const_generics.out b/charon/tests/ui/monomorphization/global_with_generics.out similarity index 100% rename from charon/tests/ui/monomorphization/const_generics.out rename to charon/tests/ui/monomorphization/global_with_generics.out diff --git a/charon/tests/ui/monomorphization/const_generics.rs b/charon/tests/ui/monomorphization/global_with_generics.rs similarity index 100% rename from charon/tests/ui/monomorphization/const_generics.rs rename to charon/tests/ui/monomorphization/global_with_generics.rs diff --git a/charon/tests/ui/simple/basic-mono.out b/charon/tests/ui/simple/basic-mono.out new file mode 100644 index 000000000..75dfaa50c --- /dev/null +++ b/charon/tests/ui/simple/basic-mono.out @@ -0,0 +1,54 @@ +# Final LLBC before serialization: + +// Full name: core::marker::MetaSized:: +#[lang_item("meta_sized")] +pub trait MetaSized:: + +// Full name: core::marker::Sized:: +#[lang_item("sized")] +pub trait Sized:: +{ + parent_clause0 : [@TraitClause0]: MetaSized:: + non-dyn-compatible +} + +// Full name: test_crate::foo::<10 : usize> +fn foo::<10 : usize>() +{ + let @0: (); // return + + @0 := () + @0 := () + return +} + +// Full name: test_crate::bar:: +fn bar::() +{ + let @0: (); // return + + @0 := () + @0 := () + return +} + +// Full name: test_crate::main +fn main() +{ + let @0: (); // return + let @1: (); // anonymous local + let @2: (); // anonymous local + + storage_live(@1) + @1 := foo::<10 : usize>() + storage_dead(@1) + storage_live(@2) + @2 := bar::() + storage_dead(@2) + @0 := () + @0 := () + return +} + + + diff --git a/charon/tests/ui/simple/basic-mono.rs b/charon/tests/ui/simple/basic-mono.rs new file mode 100644 index 000000000..a0309b875 --- /dev/null +++ b/charon/tests/ui/simple/basic-mono.rs @@ -0,0 +1,10 @@ +//@ charon-args=--monomorphize + +fn foo() {} + +fn bar() {} + +fn main() { + foo::<10>(); + bar::(); +}