From 118c7ebc4cd3e26a8cc8b8d65e8932be9a12ff19 Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Wed, 27 Nov 2024 15:08:35 +0100 Subject: [PATCH] Add a test --- .../should_succeed/syntax/int_suffix.coma | 86 ++++++++++++++++++ .../tests/should_succeed/syntax/int_suffix.rs | 7 ++ .../syntax/int_suffix/why3session.xml | 14 +++ .../syntax/int_suffix/why3shapes.gz | Bin 0 -> 183 bytes 4 files changed, 107 insertions(+) create mode 100644 creusot/tests/should_succeed/syntax/int_suffix.coma create mode 100644 creusot/tests/should_succeed/syntax/int_suffix.rs create mode 100644 creusot/tests/should_succeed/syntax/int_suffix/why3session.xml create mode 100644 creusot/tests/should_succeed/syntax/int_suffix/why3shapes.gz diff --git a/creusot/tests/should_succeed/syntax/int_suffix.coma b/creusot/tests/should_succeed/syntax/int_suffix.coma new file mode 100644 index 000000000..2e81a4cc2 --- /dev/null +++ b/creusot/tests/should_succeed/syntax/int_suffix.coma @@ -0,0 +1,86 @@ +module M_int_suffix__foo [#"int_suffix.rs" 5 0 5 29] + let%span sint_suffix0 = "int_suffix.rs" 4 10 4 25 + let%span sint_suffix1 = "int_suffix.rs" 6 11 6 15 + let%span sghost2 = "../../../../creusot-contracts/src/ghost.rs" 183 9 183 15 + let%span sint3 = "../../../../creusot-contracts/src/logic/int.rs" 28 14 28 31 + let%span sghost4 = "../../../../creusot-contracts/src/ghost.rs" 52 14 52 18 + let%span sghost5 = "../../../../creusot-contracts/src/ghost.rs" 52 4 52 36 + let%span sghost6 = "../../../../creusot-contracts/src/ghost.rs" 51 14 51 35 + let%span sghost7 = "../../../../creusot-contracts/src/ghost.rs" 147 15 147 16 + let%span sghost8 = "../../../../creusot-contracts/src/ghost.rs" 147 4 147 28 + let%span sghost9 = "../../../../creusot-contracts/src/ghost.rs" 145 14 145 28 + + use prelude.prelude.Int128 + + use prelude.prelude.Int + + type t_GhostBox'0 = + { t_GhostBox__0'0: int } + + function inner_logic'0 (self : t_GhostBox'0) : int = + [%#sghost2] self.t_GhostBox__0'0 + + use prelude.prelude.Int128 + + let rec new'0 (value:int128) (return' (ret:t_GhostBox'0))= any + [ return' (result:t_GhostBox'0)-> {[%#sint3] inner_logic'0 result = Int128.to_int value} (! return' {result}) ] + + + use prelude.prelude.Borrow + + predicate inv'0 (_1 : t_GhostBox'0) + + axiom inv_axiom'0 [@rewrite] : forall x : t_GhostBox'0 [inv'0 x] . inv'0 x = true + + predicate inv'1 (_1 : int) + + axiom inv_axiom'1 [@rewrite] : forall x : int [inv'1 x] . inv'1 x = true + + let rec deref'0 (self:t_GhostBox'0) (return' (ret:int))= {[@expl:deref 'self' type invariant] [%#sghost4] inv'0 self} + any + [ return' (result:int)-> {[%#sghost5] inv'1 result} + {[%#sghost6] self.t_GhostBox__0'0 = result} + (! return' {result}) ] + + + predicate inv'2 (_1 : int) + + axiom inv_axiom'2 [@rewrite] : forall x : int [inv'2 x] . inv'2 x = true + + predicate inv'3 (_1 : t_GhostBox'0) + + axiom inv_axiom'3 [@rewrite] : forall x : t_GhostBox'0 [inv'3 x] . inv'3 x = true + + let rec new'1 (x:int) (return' (ret:t_GhostBox'0))= {[@expl:new 'x' type invariant] [%#sghost7] inv'2 x} + any + [ return' (result:t_GhostBox'0)-> {[%#sghost8] inv'3 result} + {[%#sghost9] result.t_GhostBox__0'0 = x} + (! return' {result}) ] + + + use prelude.prelude.Intrinsic + + let rec closure1'0 (_1:()) (return' (ret:t_GhostBox'0))= bb0 + [ bb0 = s0 + [ s0 = new'0 {[%#sint_suffix1] (1 : int128)} (fun (_ret':t_GhostBox'0) -> [ &_5 <- _ret' ] s1) | s1 = bb1 ] + + | bb1 = s0 [ s0 = deref'0 {_5} (fun (_ret':int) -> [ &_3 <- _ret' ] s1) | s1 = bb2 ] + | bb2 = s0 [ s0 = new'1 {_3} (fun (_ret':t_GhostBox'0) -> [ &_0 <- _ret' ] s1) | s1 = bb3 ] + | bb3 = bb4 + | bb4 = return' {_0} ] + [ & _0 : t_GhostBox'0 = any_l () | & _3 : int = any_l () | & _5 : t_GhostBox'0 = any_l () ] + [ return' (result:t_GhostBox'0)-> return' {result} ] + + + meta "compute_max_steps" 1000000 + + let rec foo'0 (_1:()) (return' (ret:t_GhostBox'0))= (! bb0 + [ bb0 = s0 + [ s0 = [ &_2 <- () ] s1 | s1 = closure1'0 {_2} (fun (_ret':t_GhostBox'0) -> [ &_0 <- _ret' ] s2) | s2 = bb1 ] + + | bb1 = return' {_0} ] + ) [ & _0 : t_GhostBox'0 = any_l () | & _2 : () = any_l () | & _3 : () = any_l () ] + [ return' (result:t_GhostBox'0)-> {[@expl:foo ensures] [%#sint_suffix0] inner_logic'0 result = 1} + (! return' {result}) ] + +end diff --git a/creusot/tests/should_succeed/syntax/int_suffix.rs b/creusot/tests/should_succeed/syntax/int_suffix.rs new file mode 100644 index 000000000..287b186ed --- /dev/null +++ b/creusot/tests/should_succeed/syntax/int_suffix.rs @@ -0,0 +1,7 @@ +extern crate creusot_contracts; +use creusot_contracts::*; + +#[ensures(*result == 1int)] +pub fn foo() -> GhostBox { + ghost!(1int) +} diff --git a/creusot/tests/should_succeed/syntax/int_suffix/why3session.xml b/creusot/tests/should_succeed/syntax/int_suffix/why3session.xml new file mode 100644 index 000000000..823f9195c --- /dev/null +++ b/creusot/tests/should_succeed/syntax/int_suffix/why3session.xml @@ -0,0 +1,14 @@ + + + + + + + + + + + + + diff --git a/creusot/tests/should_succeed/syntax/int_suffix/why3shapes.gz b/creusot/tests/should_succeed/syntax/int_suffix/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..d882b0b858cc9ce0fb682891e9d912796e4123fa GIT binary patch literal 183 zcmV;o07(BIiwFP!00000|7DN84uUWkMfW~MHmkUbf3 zBh?aySF5(MzIHyui+^X34G$yKc^la(#PHR?Uzaai+(uvbW4sZC+%UyY{X2sYKnpEx lcvD(J?Y)p?bFffKCa81;l~`!5nWma(Kws(`7gz)V002@4O+^3z literal 0 HcmV?d00001