diff --git a/creusot-contracts/src/std/boxed.rs b/creusot-contracts/src/std/boxed.rs index 804c110dbd..2e65842d17 100644 --- a/creusot-contracts/src/std/boxed.rs +++ b/creusot-contracts/src/std/boxed.rs @@ -3,11 +3,11 @@ pub use ::std::boxed::*; #[cfg(creusot)] impl DeepModel for Box { - type DeepModelTy = T::DeepModelTy; + type DeepModelTy = Box; #[ghost] #[open] fn deep_model(self) -> Self::DeepModelTy { - (*self).deep_model() + Box::new((*self).deep_model()) } } diff --git a/creusot/tests/should_succeed/syntax/derive_macros.mlcfg b/creusot/tests/should_succeed/syntax/derive_macros.mlcfg index af6d045fa2..d831fd0b99 100644 --- a/creusot/tests/should_succeed/syntax/derive_macros.mlcfg +++ b/creusot/tests/should_succeed/syntax/derive_macros.mlcfg @@ -1270,6 +1270,210 @@ module DeriveMacros_Impl7_Resolve val resolve [#"../derive_macros.rs" 56 9 56 16] (self : DeriveMacros_Sum2_Type.t_sum2 a b) : bool ensures { result = resolve self } +end +module Core_Option_Option_Type + type t_option 't = + | C_None + | C_Some 't + +end +module DeriveMacros_List_Type + use Core_Option_Option_Type as Core_Option_Option_Type + type t_list 't = + | C_List 't (Core_Option_Option_Type.t_option (t_list 't)) + + let function list_elem (self : t_list 't) : 't = [@vc:do_not_keep_trace] [@vc:sp] + match (self) with + | C_List a _ -> a + end + let function list_tail (self : t_list 't) : Core_Option_Option_Type.t_option (t_list 't) + = [@vc:do_not_keep_trace] [@vc:sp] + match (self) with + | C_List _ a -> a + end +end +module DeriveMacros_ListDeepModel_Type + use Core_Option_Option_Type as Core_Option_Option_Type + type t_listdeepmodel 't 'proj0 = + | C_ListDeepModel 'proj0 (Core_Option_Option_Type.t_option (t_listdeepmodel 't 'proj0)) + +end +module CreusotContracts_Std1_Option_Impl0_DeepModel_Stub + type t + clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with + type self = t + use Core_Option_Option_Type as Core_Option_Option_Type + function deep_model (self : Core_Option_Option_Type.t_option t) : Core_Option_Option_Type.t_option DeepModelTy0.deepModelTy + +end +module CreusotContracts_Std1_Option_Impl0_DeepModel_Interface + type t + clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with + type self = t + use Core_Option_Option_Type as Core_Option_Option_Type + function deep_model (self : Core_Option_Option_Type.t_option t) : Core_Option_Option_Type.t_option DeepModelTy0.deepModelTy + + val deep_model (self : Core_Option_Option_Type.t_option t) : Core_Option_Option_Type.t_option DeepModelTy0.deepModelTy + ensures { result = deep_model self } + +end +module CreusotContracts_Std1_Option_Impl0_DeepModel + type t + clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with + type self = t + clone CreusotContracts_Model_DeepModel_DeepModel_Stub as DeepModel0 with + type self = t, + type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy + use Core_Option_Option_Type as Core_Option_Option_Type + function deep_model (self : Core_Option_Option_Type.t_option t) : Core_Option_Option_Type.t_option DeepModelTy0.deepModelTy + + = + [#"../../../../../creusot-contracts/src/std/option.rs" 10 8 13 9] match (self) with + | Core_Option_Option_Type.C_Some t -> Core_Option_Option_Type.C_Some (DeepModel0.deep_model t) + | Core_Option_Option_Type.C_None -> Core_Option_Option_Type.C_None + end + val deep_model (self : Core_Option_Option_Type.t_option t) : Core_Option_Option_Type.t_option DeepModelTy0.deepModelTy + ensures { result = deep_model self } + +end +module Alloc_Boxed_Box_Type + use Core_Ptr_Unique_Unique_Type as Core_Ptr_Unique_Unique_Type + type t_box 't 'a = + | C_Box (Core_Ptr_Unique_Unique_Type.t_unique 't) 'a + +end +module DeriveMacros_Impl8_DeepModel_Stub + type t + clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with + type self = t + use DeriveMacros_ListDeepModel_Type as DeriveMacros_ListDeepModel_Type + use DeriveMacros_List_Type as DeriveMacros_List_Type + function deep_model [#"../derive_macros.rs" 62 9 62 18] (self : DeriveMacros_List_Type.t_list t) : DeriveMacros_ListDeepModel_Type.t_listdeepmodel t DeepModelTy0.deepModelTy + +end +module DeriveMacros_Impl8_DeepModel_Interface + type t + clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with + type self = t + use DeriveMacros_ListDeepModel_Type as DeriveMacros_ListDeepModel_Type + use DeriveMacros_List_Type as DeriveMacros_List_Type + function deep_model [#"../derive_macros.rs" 62 9 62 18] (self : DeriveMacros_List_Type.t_list t) : DeriveMacros_ListDeepModel_Type.t_listdeepmodel t DeepModelTy0.deepModelTy + + val deep_model [#"../derive_macros.rs" 62 9 62 18] (self : DeriveMacros_List_Type.t_list t) : DeriveMacros_ListDeepModel_Type.t_listdeepmodel t DeepModelTy0.deepModelTy + ensures { result = deep_model self } + +end +module DeriveMacros_Impl8_DeepModel + type t + use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type + clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with + type self = t + use DeriveMacros_ListDeepModel_Type as DeriveMacros_ListDeepModel_Type + use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type + use Core_Option_Option_Type as Core_Option_Option_Type + use DeriveMacros_List_Type as DeriveMacros_List_Type + clone CreusotContracts_Std1_Option_Impl0_DeepModel_Stub as DeepModel1 with + type t = DeriveMacros_List_Type.t_list t, + type DeepModelTy0.deepModelTy = DeriveMacros_ListDeepModel_Type.t_listdeepmodel t DeepModelTy0.deepModelTy + clone CreusotContracts_Model_DeepModel_DeepModel_Stub as DeepModel0 with + type self = t, + type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy + function deep_model [#"../derive_macros.rs" 62 9 62 18] (self : DeriveMacros_List_Type.t_list t) : DeriveMacros_ListDeepModel_Type.t_listdeepmodel t DeepModelTy0.deepModelTy + + = + [#"../derive_macros.rs" 62 9 729 44] DeriveMacros_ListDeepModel_Type.C_ListDeepModel (DeepModel0.deep_model (DeriveMacros_List_Type.list_elem self)) (DeepModel1.deep_model (DeriveMacros_List_Type.list_tail self)) + val deep_model [#"../derive_macros.rs" 62 9 62 18] (self : DeriveMacros_List_Type.t_list t) : DeriveMacros_ListDeepModel_Type.t_listdeepmodel t DeepModelTy0.deepModelTy + ensures { result = deep_model self } + +end +module DeriveMacros_Expr_Type + type t_expr 'v = + | C_Var 'v + | C_Add (t_expr 'v) (t_expr 'v) + +end +module DeriveMacros_ExprDeepModel_Type + type t_exprdeepmodel 'v 'proj0 = + | C_Var 'proj0 + | C_Add (t_exprdeepmodel 'v 'proj0) (t_exprdeepmodel 'v 'proj0) + +end +module CreusotContracts_Std1_Boxed_Impl0_DeepModel_Stub + type t + type a + clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with + type self = t + function deep_model (self : t) : DeepModelTy0.deepModelTy +end +module CreusotContracts_Std1_Boxed_Impl0_DeepModel_Interface + type t + type a + clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with + type self = t + function deep_model (self : t) : DeepModelTy0.deepModelTy + val deep_model (self : t) : DeepModelTy0.deepModelTy + ensures { result = deep_model self } + +end +module CreusotContracts_Std1_Boxed_Impl0_DeepModel + type t + type a + clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with + type self = t + clone CreusotContracts_Model_DeepModel_DeepModel_Stub as DeepModel0 with + type self = t, + type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy + function deep_model (self : t) : DeepModelTy0.deepModelTy = + [#"../../../../../creusot-contracts/src/std/boxed.rs" 10 17 10 37] DeepModel0.deep_model self + val deep_model (self : t) : DeepModelTy0.deepModelTy + ensures { result = deep_model self } + +end +module DeriveMacros_Impl9_DeepModel_Stub + type v + clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with + type self = v + use DeriveMacros_ExprDeepModel_Type as DeriveMacros_ExprDeepModel_Type + use DeriveMacros_Expr_Type as DeriveMacros_Expr_Type + function deep_model [#"../derive_macros.rs" 68 9 68 18] (self : DeriveMacros_Expr_Type.t_expr v) : DeriveMacros_ExprDeepModel_Type.t_exprdeepmodel v DeepModelTy0.deepModelTy + +end +module DeriveMacros_Impl9_DeepModel_Interface + type v + clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with + type self = v + use DeriveMacros_ExprDeepModel_Type as DeriveMacros_ExprDeepModel_Type + use DeriveMacros_Expr_Type as DeriveMacros_Expr_Type + function deep_model [#"../derive_macros.rs" 68 9 68 18] (self : DeriveMacros_Expr_Type.t_expr v) : DeriveMacros_ExprDeepModel_Type.t_exprdeepmodel v DeepModelTy0.deepModelTy + + val deep_model [#"../derive_macros.rs" 68 9 68 18] (self : DeriveMacros_Expr_Type.t_expr v) : DeriveMacros_ExprDeepModel_Type.t_exprdeepmodel v DeepModelTy0.deepModelTy + ensures { result = deep_model self } + +end +module DeriveMacros_Impl9_DeepModel + type v + use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type + clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with + type self = v + use DeriveMacros_ExprDeepModel_Type as DeriveMacros_ExprDeepModel_Type + use DeriveMacros_Expr_Type as DeriveMacros_Expr_Type + clone CreusotContracts_Std1_Boxed_Impl0_DeepModel_Stub as DeepModel1 with + type t = DeriveMacros_Expr_Type.t_expr v, + type a = Alloc_Alloc_Global_Type.t_global, + type DeepModelTy0.deepModelTy = DeriveMacros_ExprDeepModel_Type.t_exprdeepmodel v DeepModelTy0.deepModelTy + clone CreusotContracts_Model_DeepModel_DeepModel_Stub as DeepModel0 with + type self = v, + type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy + function deep_model [#"../derive_macros.rs" 68 9 68 18] (self : DeriveMacros_Expr_Type.t_expr v) : DeriveMacros_ExprDeepModel_Type.t_exprdeepmodel v DeepModelTy0.deepModelTy + + = + [#"../derive_macros.rs" 68 9 68 18] match (self) with + | DeriveMacros_Expr_Type.C_Var v0_1 -> DeriveMacros_ExprDeepModel_Type.C_Var (DeepModel0.deep_model v0_1) + | DeriveMacros_Expr_Type.C_Add v0_1 v1_1 -> DeriveMacros_ExprDeepModel_Type.C_Add (DeepModel1.deep_model v0_1) (DeepModel1.deep_model v1_1) + end + val deep_model [#"../derive_macros.rs" 68 9 68 18] (self : DeriveMacros_Expr_Type.t_expr v) : DeriveMacros_ExprDeepModel_Type.t_exprdeepmodel v DeepModelTy0.deepModelTy + ensures { result = deep_model self } + end module DeriveMacros_Impl2 type a @@ -1385,6 +1589,12 @@ module DeriveMacros_Impl1 type a type b end +module DeriveMacros_Impl8 + type t +end +module DeriveMacros_Impl9 + type v +end module DeriveMacros_Impl6 type a end diff --git a/creusot/tests/should_succeed/syntax/derive_macros.rs b/creusot/tests/should_succeed/syntax/derive_macros.rs index c6afd02806..ff5df83114 100644 --- a/creusot/tests/should_succeed/syntax/derive_macros.rs +++ b/creusot/tests/should_succeed/syntax/derive_macros.rs @@ -58,3 +58,15 @@ pub enum Sum2 { X(A), Y { a: bool, x: B }, } + +#[derive(DeepModel)] +pub struct List { + pub elem: T, + pub tail : Option>>, +} + +#[derive(DeepModel)] +pub enum Expr { + Var(V), + Add(Box>, Box>), +} \ No newline at end of file