Skip to content

Commit

Permalink
bless
Browse files Browse the repository at this point in the history
  • Loading branch information
@dewert99
dewert99 committed Jul 26, 2024
1 parent 15512bc commit a6f23ef
Show file tree
Hide file tree
Showing 57 changed files with 11,938 additions and 19,579 deletions.
122 changes: 38 additions & 84 deletions creusot/tests/should_fail/bug/01_resolve_unsoundness.coma
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,22 +101,7 @@ module Alloc_Alloc_Global_Type

end
module CreusotContracts_Logic_Seq2_Seq_Type
use seq.Seq

type t_seq 't =
| C_Seq (Seq.seq 't)

function any_l (_ : 'b) : 'a

let rec t_seq < 't > (input:t_seq 't) (ret (field_0:Seq.seq 't))= any
[ good (field_0:Seq.seq 't)-> {C_Seq field_0 = input} (! ret {field_0})
| bad (field_0:Seq.seq 't)-> {C_Seq field_0 <> input} {false} any ]


function seq_0 [@inline:trivial] (self : t_seq 't) : Seq.seq 't =
match self with
| C_Seq a -> a
end
type t_seq 't
end
module C01ResolveUnsoundness_MakeVecOfSize
let%span s01_resolve_unsoundness0 = "../01_resolve_unsoundness.rs" 10 29 10 39
Expand All @@ -135,55 +120,39 @@ module C01ResolveUnsoundness_MakeVecOfSize

let%span span7 = "" 0 0 0 0

let%span span8 = "../../../../../creusot-contracts/src/logic/seq2.rs" 72 15 72 19

let%span span9 = "../../../../../creusot-contracts/src/logic/seq2.rs" 71 14 71 25

let%span span10 = "../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25

let%span span11 = "../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41

let%span span12 = "../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36
let%span span8 = "../../../../../creusot-contracts/src/logic/seq2.rs" 68 14 68 25

let%span span13 = "../../../../../creusot-contracts/src/std/vec.rs" 60 20 60 41
let%span span9 = "../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25

let%span span14 = "../../../../../creusot-contracts/src/logic/seq2.rs" 19 4 19 25
let%span span10 = "../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41

let%span span15 = "../../../../../creusot-contracts/src/logic/seq2.rs" 23 14 23 36
let%span span11 = "../../../../../creusot-contracts/src/std/vec.rs" 60 20 60 41

let%span span16 = "../../../../../creusot-contracts/src/logic/seq2.rs" 21 4 21 10
let%span span12 = "../../../../../creusot-contracts/src/logic/seq2.rs" 16 14 16 36

let%span span17 = "../../../../../creusot-contracts/src/logic/seq2.rs" 107 18 107 22
let%span span13 = "../../../../../creusot-contracts/src/logic/seq2.rs" 104 14 104 54

let%span span18 = "../../../../../creusot-contracts/src/logic/seq2.rs" 107 24 107 29
let%span span14 = "../../../../../creusot-contracts/src/logic/seq2.rs" 105 4 106 62

let%span span19 = "../../../../../creusot-contracts/src/logic/seq2.rs" 104 14 104 54
let%span span15 = "../../../../../creusot-contracts/src/logic/seq2.rs" 54 21 54 22

let%span span20 = "../../../../../creusot-contracts/src/logic/seq2.rs" 105 4 106 62
let%span span16 = "../../../../../creusot-contracts/src/logic/seq2.rs" 52 14 52 31

let%span span21 = "../../../../../creusot-contracts/src/logic/seq2.rs" 107 4 107 44
let%span span17 = "../../../../../creusot-contracts/src/logic/seq2.rs" 53 14 53 28

let%span span22 = "../../../../../creusot-contracts/src/logic/seq2.rs" 58 21 58 22
let%span span18 = "../../../../../creusot-contracts/src/logic/seq2.rs" 98 8 98 39

let%span span23 = "../../../../../creusot-contracts/src/logic/seq2.rs" 56 14 56 31
let%span span19 = "../../../../../creusot-contracts/src/model.rs" 108 8 108 31

let%span span24 = "../../../../../creusot-contracts/src/logic/seq2.rs" 57 14 57 28
let%span span20 = "" 0 0 0 0

let%span span25 = "../../../../../creusot-contracts/src/logic/seq2.rs" 58 4 58 34
let%span span21 = "" 0 0 0 0

let%span span26 = "../../../../../creusot-contracts/src/logic/seq2.rs" 99 8 99 39
let%span span22 = "../../../../../creusot-contracts/src/std/vec.rs" 82 26 82 51

let%span span27 = "../../../../../creusot-contracts/src/model.rs" 108 8 108 31
let%span span23 = "../../../../../creusot-contracts/src/std/vec.rs" 69 26 69 44

let%span span28 = "" 0 0 0 0

let%span span29 = "" 0 0 0 0

let%span span30 = "../../../../../creusot-contracts/src/std/vec.rs" 82 26 82 51

let%span span31 = "../../../../../creusot-contracts/src/std/vec.rs" 69 26 69 44

let%span span32 = "" 0 0 0 0
let%span span24 = "" 0 0 0 0

use CreusotContracts_Logic_Seq2_Seq_Type as Seq'0

Expand Down Expand Up @@ -222,76 +191,61 @@ module C01ResolveUnsoundness_MakeVecOfSize

constant max'0 : usize = [%#span7] (18446744073709551615 : usize)

use seq.Seq

use CreusotContracts_Logic_Seq2_Seq_Type as CreusotContracts_Logic_Seq2_Seq_Type

function len'0 (self : Seq'0.t_seq bool) : int

axiom len'0_spec : forall self : Seq'0.t_seq bool . ([%#span8] inv'3 self) -> ([%#span9] len'0 self >= 0)
axiom len'0_spec : forall self : Seq'0.t_seq bool . [%#span8] len'0 self >= 0

predicate inv'0 (_x : Vec'0.t_vec bool (Global'0.t_global))

function shallow_model'0 (self : Vec'0.t_vec bool (Global'0.t_global)) : Seq'0.t_seq bool

axiom shallow_model'0_spec : forall self : Vec'0.t_vec bool (Global'0.t_global) . ([%#span10] inv'0 self)
-> ([%#span12] inv'3 (shallow_model'0 self))
&& ([%#span11] len'0 (shallow_model'0 self) <= UIntSize.to_int (max'0 : usize))
axiom shallow_model'0_spec : forall self : Vec'0.t_vec bool (Global'0.t_global) . ([%#span9] inv'0 self)
-> ([%#span10] len'0 (shallow_model'0 self) <= UIntSize.to_int (max'0 : usize))

predicate invariant'0 (self : Vec'0.t_vec bool (Global'0.t_global)) =
[%#span13] inv'3 (shallow_model'0 self)
[%#span11] inv'3 (shallow_model'0 self)

axiom inv'0 : forall x : Vec'0.t_vec bool (Global'0.t_global) . inv'0 x = true

constant empty'0 : Seq'0.t_seq bool = [%#span14] ()
constant empty'0 : Seq'0.t_seq bool

function empty_len'0 (_1 : ()) : () =
[%#span16] ()
function empty_len'0 (_1 : ()) : ()

axiom empty_len'0_spec : forall _1 : () . [%#span15] len'0 (empty'0 : Seq'0.t_seq bool) = 0
axiom empty_len'0_spec : forall _1 : () . [%#span12] len'0 (empty'0 : Seq'0.t_seq bool) = 0

use prelude.prelude.Intrinsic

use seq.Seq

use seq.Seq

function index_logic'0 (self : Seq'0.t_seq bool) (x : int) : bool
function index_logic'0 (self : Seq'0.t_seq bool) (_2 : int) : bool

function concat'0 (self : Seq'0.t_seq bool) (other : Seq'0.t_seq bool) : Seq'0.t_seq bool

axiom concat'0_spec : forall self : Seq'0.t_seq bool, other : Seq'0.t_seq bool . ([%#span17] inv'3 self)
-> ([%#span18] inv'3 other)
-> ([%#span21] inv'3 (concat'0 self other))
&& ([%#span20] forall i : int . 0 <= i /\ i < len'0 (concat'0 self other)
axiom concat'0_spec : forall self : Seq'0.t_seq bool, other : Seq'0.t_seq bool . ([%#span14] forall i : int . 0 <= i
/\ i < len'0 (concat'0 self other)
-> index_logic'0 (concat'0 self other) i
= (if i < len'0 self then index_logic'0 self i else index_logic'0 other (i - len'0 self)))
&& ([%#span19] len'0 (concat'0 self other) = len'0 self + len'0 other)

use seq.Seq
&& ([%#span13] len'0 (concat'0 self other) = len'0 self + len'0 other)

function singleton'0 (v : bool) : Seq'0.t_seq bool

axiom singleton'0_spec : forall v : bool . ([%#span22] inv'2 v)
-> ([%#span25] inv'3 (singleton'0 v))
&& ([%#span24] index_logic'0 (singleton'0 v) 0 = v) && ([%#span23] len'0 (singleton'0 v) = 1)
axiom singleton'0_spec : forall v : bool . ([%#span15] inv'2 v)
-> ([%#span17] index_logic'0 (singleton'0 v) 0 = v) && ([%#span16] len'0 (singleton'0 v) = 1)

function push'1 [@inline:trivial] (self : Seq'0.t_seq bool) (v : bool) : Seq'0.t_seq bool =
[%#span26] concat'0 self (singleton'0 v)
[%#span18] concat'0 self (singleton'0 v)

function shallow_model'1 (self : borrowed (Vec'0.t_vec bool (Global'0.t_global))) : Seq'0.t_seq bool =
[%#span27] shallow_model'0 ( * self)
[%#span19] shallow_model'0 ( * self)

let rec push'0 (self:borrowed (Vec'0.t_vec bool (Global'0.t_global))) (value:bool) (return' (ret:()))= {[@expl:precondition] [%#span29] inv'2 value}
{[@expl:precondition] [%#span28] inv'1 self}
let rec push'0 (self:borrowed (Vec'0.t_vec bool (Global'0.t_global))) (value:bool) (return' (ret:()))= {[@expl:precondition] [%#span21] inv'2 value}
{[@expl:precondition] [%#span20] inv'1 self}
any
[ return' (result:())-> {[%#span30] shallow_model'0 ( ^ self) = push'1 (shallow_model'1 self) value}
[ return' (result:())-> {[%#span22] shallow_model'0 ( ^ self) = push'1 (shallow_model'1 self) value}
(! return' {result}) ]


let rec new'0 (_1:()) (return' (ret:Vec'0.t_vec bool (Global'0.t_global)))= any
[ return' (result:Vec'0.t_vec bool (Global'0.t_global))-> {[%#span32] inv'0 result}
{[%#span31] len'0 (shallow_model'0 result) = 0}
[ return' (result:Vec'0.t_vec bool (Global'0.t_global))-> {[%#span24] inv'0 result}
{[%#span23] len'0 (shallow_model'0 result) = 0}
(! return' {result}) ]


Expand Down
Loading

0 comments on commit a6f23ef

Please sign in to comment.