silicon
silicon copied to clipboard
viperproject
Trigger selection fails for expressions with let bindings
The following example fails to verify, even though it's essentially trying to prove forall i: Int :: ... ==> i >= i:
domain s_UInt_u32 {
function s_UInt_u32_value(arg0: s_UInt_u32): Int
function s_UInt_u32_cons(arg0: Int): s_UInt_u32
axiom s_UInt_u32_ax_cons {
(forall s: s_UInt_u32 ::
{ s_UInt_u32_value(s) }
s_UInt_u32_cons(s_UInt_u32_value(s)) == s)
}
axiom s_UInt_u32_ax_bounds {
(forall s: s_UInt_u32 ::
{ s_UInt_u32_value(s) }
0 <= s_UInt_u32_value(s) && s_UInt_u32_value(s) <= 4294967295)
}
axiom s_UInt_u32_ax_value {
(forall value: Int ::
{ s_UInt_u32_cons(value) }
0 <= value && value <= 4294967295 ==>
s_UInt_u32_value(s_UInt_u32_cons(value)) == value)
}
}
domain s_Bool {
function s_Bool_value(arg0: s_Bool): Bool
function s_Bool_cons(arg0: Bool): s_Bool
axiom s_Bool_ax_cons {
(forall s: s_Bool ::
{ s_Bool_value(s) }
s_Bool_cons(s_Bool_value(s)) == s)
}
axiom s_Bool_ax_value {
(forall value: Bool ::
{ s_Bool_cons(value) }
s_Bool_value(s_Bool_cons(value)) == value)
}
}
domain s_Param {
}
domain TypeOf {
function s_Param_typeof(arg0: s_Param): Type
function s_Fields_typeof(arg0: s_Fields): Type
function s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0_typeof(arg0: s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0): Type
function s_Ref_immutable_typeof(arg0: s_Ref_immutable): Type
function s_UInt_u32_typeof(arg0: s_UInt_u32): Type
function s_Bool_typeof(arg0: s_Bool): Type
}
field p_UInt_u32_val: s_UInt_u32
field p_Ref_immutable_val: s_Ref_immutable
function f_Fields$colon$$colon$get_field_1(_1p: s_Ref_immutable): s_UInt_u32
{
(let _0_1s_bb0_s0_i0 ==
(_1p) in
(let _0_0s_bb0_s0_i0 ==
(make_concrete_s_Fields(_0_1s_bb0_s0_i0.s_Ref_immutable_1).s_Fields_0) in
_0_0s_bb0_s0_i0))
}
function mir_binop_Ge_u32_u32(arg1: s_UInt_u32, arg2: s_UInt_u32): s_Bool
{
s_Bool_cons(s_UInt_u32_value(arg1) >= s_UInt_u32_value(arg2))
}
function make_generic_s_Fields(self: s_Fields): s_Param
ensures make_concrete_s_Fields(result) == self
function make_concrete_s_Fields(snap: s_Param): s_Fields
ensures make_generic_s_Fields(result) == snap
function make_generic_s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0(self: s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0): s_Param
ensures make_concrete_s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0(result) ==
self
function make_concrete_s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0(snap: s_Param): s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0
ensures make_generic_s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0(result) ==
snap
function make_generic_s_Bool(self: s_Bool): s_Param
ensures make_concrete_s_Bool(result) == self
function make_concrete_s_Bool(snap: s_Param): s_Bool
ensures make_generic_s_Bool(result) == snap
function s_UInt_u32_unreachable(): s_UInt_u32
requires false
ensures false
function s_0_Tuple_unreachable(): s_0_Tuple
requires false
ensures false
function s_Fields_unreachable(): s_Fields
requires false
ensures false
function s_Bool_unreachable(): s_Bool
requires false
ensures false
function s_Ref_immutable_unreachable(): s_Ref_immutable
requires false
ensures false
function s_Param_unreachable(): s_Param
requires false
ensures false
function s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0_unreachable(): s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0
requires false
ensures false
function s_1_Tuple_unreachable(): s_1_Tuple
requires false
ensures false
function p_UInt_u32_snap(self: Ref): s_UInt_u32
requires acc(p_UInt_u32(self), write)
{
(unfolding acc(p_UInt_u32(self), write) in self.p_UInt_u32_val)
}
function p_0_Tuple_snap(self: Ref): s_0_Tuple
requires acc(p_0_Tuple(self), write)
{
(unfolding acc(p_0_Tuple(self), write) in s_0_Tuple_cons())
}
function p_Fields_field_0(self: Ref): Ref
ensures (self == null) == (result == null)
function p_Fields_field_1(self: Ref): Ref
ensures (self == null) == (result == null)
function p_Fields_snap(self: Ref): s_Fields
requires acc(p_Fields(self), write)
{
(unfolding acc(p_Fields(self), write) in
s_Fields_cons(p_UInt_u32_snap(p_Fields_field_0(self)), p_0_Tuple_snap(p_Fields_field_1(self))))
}
function p_Ref_immutable_deref(self: Ref, T: Type): Ref
requires acc(p_Ref_immutable(self, T), write)
{
(unfolding acc(p_Ref_immutable(self, T), write) in
self.p_Ref_immutable_val.s_Ref_immutable_0)
}
function p_Ref_immutable_snap(self: Ref, T: Type): s_Ref_immutable
requires acc(p_Ref_immutable(self, T), write)
ensures s_Param_typeof(result.s_Ref_immutable_1) == T
{
(unfolding acc(p_Ref_immutable(self, T), write) in
self.p_Ref_immutable_val)
}
function p_Param_snap(self: Ref, T: Type): s_Param
function p_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0_field_0(self: Ref): Ref
ensures (self == null) == (result == null)
function p_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0_snap(self: Ref): s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0
requires acc(p_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0(self), write)
{
(unfolding acc(p_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0(self), write) in
s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0_cons(p_Ref_immutable_snap(p_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0_field_0(self),
s_Fields_type())))
}
predicate p_UInt_u32(self: Ref) {
acc(self.p_UInt_u32_val, write)
}
predicate p_0_Tuple(self: Ref) {
true
}
predicate p_Fields(self: Ref) {
acc(p_UInt_u32(p_Fields_field_0(self)), write) &&
acc(p_0_Tuple(p_Fields_field_1(self)), write)
}
predicate p_Ref_immutable(self: Ref, T: Type) {
acc(self.p_Ref_immutable_val, write) &&
s_Param_typeof(self.p_Ref_immutable_val.s_Ref_immutable_1) == T
}
predicate p_Param(self: Ref, T: Type)
predicate p_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0(self: Ref) {
acc(p_Ref_immutable(p_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0_field_0(self),
s_Fields_type()), write)
}
method m_test(_0p: Ref)
ensures acc(p_Fields(_0p), write)
ensures s_Bool_value((let _0_1s_bb0_s0_i0 ==
(p_Fields_snap(_0p)) in
(let _0_3s_bb0_s2_i1 ==
(s_0_Tuple_cons()) in
(let _0_7s_bb0_s7_i1 ==
(s_Ref_immutable_cons(null, make_generic_s_Fields(_0_1s_bb0_s0_i0))) in
(let _0_6s_bb0_s8_i1 ==
(s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0_cons(_0_7s_bb0_s7_i1)) in
(let _0_5s_bb0_s10_i1 ==
(s_Ref_immutable_cons(null, make_generic_s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0(_0_6s_bb0_s8_i1))) in
(let _0_4s_bb0_s11_i1 ==
(s_Ref_immutable_cons(null, make_generic_s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0(make_concrete_s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0(_0_5s_bb0_s10_i1.s_Ref_immutable_1)))) in
(let _0_2s_bb0_s12_i1 ==
(s_Bool_cons((forall qvar_0_0: s_UInt_u32 ::s_Bool_value((let _1_1s_bb0_s0_i0 ==
(_0_4s_bb0_s11_i1) in
(let _1_2s_bb0_s0_i0 ==
(qvar_0_0) in
(let _1_4s_bb0_s2_i1 ==
(_1_2s_bb0_s0_i0) in
(let _1_6s_bb0_s5_i1 ==
(s_Ref_immutable_cons(null, make_generic_s_Fields(make_concrete_s_Fields(make_concrete_s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0(_1_1s_bb0_s0_i0.s_Ref_immutable_1).s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0_0.s_Ref_immutable_1)))) in
(let _1_5s_bb0_s6_i1 ==
(f_Fields$colon$$colon$get_field_1(_1_6s_bb0_s5_i1)) in
(let _1_3s_bb1_s1_i1 ==
(mir_binop_Ge_u32_u32(_1_4s_bb0_s2_i1, _1_5s_bb0_s6_i1)) in
(let _1_phi_bb1_s2_i0 ==
((s_Bool_value(_1_3s_bb1_s1_i1) == false ?
(let _1_0s_bb3_s2_i0 ==
(s_Bool_cons(true)) in
s_1_Tuple_cons(make_generic_s_Bool(_1_0s_bb3_s2_i0))) :
(let _1_7s_bb2_s3_i1 ==
(_1_2s_bb0_s0_i0) in
(let _1_8s_bb2_s5_i1 ==
(_1_2s_bb0_s0_i0) in
(let _1_0s_bb2_s6_i1 ==
(mir_binop_Ge_u32_u32(_1_7s_bb2_s3_i1,
_1_8s_bb2_s5_i1)) in
s_1_Tuple_cons(make_generic_s_Bool(_1_0s_bb2_s6_i1))))))) in
(let _1_0s_bb1_s2_i2 ==
(make_concrete_s_Bool(_1_phi_bb1_s2_i0.s_1_Tuple_0)) in
_1_0s_bb1_s2_i2)))))))))))) in
(let _0_0s_bb1_s6_i0 ==
(_0_2s_bb0_s12_i1) in
_0_0s_bb1_s6_i0)))))))))
{
var _1p: Ref
var _tmp0: s_0_Tuple
label start
// var _1p
goto bb_0
label bb_0
// [MIR] bb0[0]: StorageLive(_1)
// [MIR] bb0[1]: _1 = ()
// (ignoring)
// (ignoring)
// (ignoring)
p_0_Tuple_assign(_1p, s_0_Tuple_cons())
label _after_0_1
// [MIR] bb0[2]: _0 = Fields { field_1: const 0_u32, field_2: move _1 }
// (ignoring)
// (ignoring)
// (ignoring)
// (ignoring)
// (ignoring)
// var _tmp0
_tmp0 := p_0_Tuple_snap(_1p)
exhale acc(p_0_Tuple(_1p), write)
p_Fields_assign(_0p, s_Fields_cons(s_UInt_u32_cons(0), _tmp0))
label _after_0_2
// [MIR] bb0[3]: StorageDead(_1)
// (ignoring)
// [MIR] bb0[4]: return
// PCG (T) pre_operands
// PCG (T) post_operands
// PCG (T) pre_main
// PCG (T) post_main
label package_post0
label _after_0_4
goto end
label end
// return
}
method make_generic_p_Fields(self: Ref)
requires acc(p_Fields(self), write)
ensures acc(p_Param(self, s_Fields_type()), write)
ensures old(make_generic_s_Fields(p_Fields_snap(self))) ==
p_Param_snap(self, s_Fields_type())
method make_concrete_p_Fields(self: Ref)
requires acc(p_Param(self, s_Fields_type()), write)
ensures acc(p_Fields(self), write)
ensures old(p_Param_snap(self, s_Fields_type())) ==
make_generic_s_Fields(p_Fields_snap(self))
method p_UInt_u32_assign(self: Ref, value: s_UInt_u32)
ensures acc(p_UInt_u32(self), write)
ensures p_UInt_u32_snap(self) == value
method p_0_Tuple_assign(self: Ref, value: s_0_Tuple)
ensures acc(p_0_Tuple(self), write)
ensures p_0_Tuple_snap(self) == value
method p_Fields_assign(self: Ref, value: s_Fields)
ensures acc(p_Fields(self), write)
ensures p_Fields_snap(self) == value
method p_Ref_immutable_assign(self: Ref, T: Type, value: s_Ref_immutable)
ensures acc(p_Ref_immutable(self, T), write)
ensures p_Ref_immutable_snap(self, T) == value
method p_Param_assign(self: Ref, T: Type, value: s_Param)
ensures acc(p_Param(self, T), write)
ensures p_Param_snap(self, T) == value
method p_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0_assign(self: Ref,
value: s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0)
ensures acc(p_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0(self), write)
ensures p_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0_snap(self) ==
value
adt s_0_Tuple {
s_0_Tuple_cons()
}
adt s_Fields {
s_Fields_cons(s_Fields_0: s_UInt_u32, s_Fields_1: s_0_Tuple)
}
adt s_Ref_immutable {
s_Ref_immutable_cons(s_Ref_immutable_0: Ref, s_Ref_immutable_1: s_Param)
}
adt s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0 {
s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0_cons(s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0_0: s_Ref_immutable)
}
adt s_1_Tuple {
s_1_Tuple_cons(s_1_Tuple_0: s_Param)
}
adt Type {
s_Fields_type()
s_prusti_post_item_test_80e8859f35b741c5b05447b46d6b38fa_Closure_0_type()
s_Ref_immutable_type(s_Ref_immutable_typaram_T: Type)
s_UInt_u32_type()
s_Bool_type()
Unknown_type(non_unit: Int)
}
Here is an example where adding a { mir_binop_Ge_u32_u32(qvar_0_0, qvar_0_0) } trigger makes it pass.
domain s_UInt_u32 {
function s_UInt_u32_value(arg0: s_UInt_u32): Int
function s_UInt_u32_cons(arg0: Int): s_UInt_u32
axiom s_UInt_u32_ax_cons {
(forall s: s_UInt_u32 ::
{ s_UInt_u32_value(s) }
s_UInt_u32_cons(s_UInt_u32_value(s)) == s)
}
axiom s_UInt_u32_ax_bounds {
(forall s: s_UInt_u32 ::
{ s_UInt_u32_value(s) }
0 <= s_UInt_u32_value(s) && s_UInt_u32_value(s) <= 4294967295)
}
axiom s_UInt_u32_ax_value {
(forall value: Int ::
{ s_UInt_u32_cons(value) }
0 <= value && value <= 4294967295 ==>
s_UInt_u32_value(s_UInt_u32_cons(value)) == value)
}
}
domain s_Int_i8 {
function s_Int_i8_value(arg0: s_Int_i8): Int
function s_Int_i8_cons(arg0: Int): s_Int_i8
axiom s_Int_i8_ax_cons {
(forall s: s_Int_i8 ::
{ s_Int_i8_value(s) }
s_Int_i8_cons(s_Int_i8_value(s)) == s)
}
axiom s_Int_i8_ax_bounds {
(forall s: s_Int_i8 ::
{ s_Int_i8_value(s) }
-128 <= s_Int_i8_value(s) && s_Int_i8_value(s) <= 127)
}
axiom s_Int_i8_ax_value {
(forall value: Int ::
{ s_Int_i8_cons(value) }
-128 <= value && value <= 127 ==>
s_Int_i8_value(s_Int_i8_cons(value)) == value)
}
}
domain s_Param {
}
domain s_Bool {
function s_Bool_value(arg0: s_Bool): Bool
function s_Bool_cons(arg0: Bool): s_Bool
axiom s_Bool_ax_cons {
(forall s: s_Bool ::
{ s_Bool_value(s) }
s_Bool_cons(s_Bool_value(s)) == s)
}
axiom s_Bool_ax_value {
(forall value: Bool ::
{ s_Bool_cons(value) }
s_Bool_value(s_Bool_cons(value)) == value)
}
}
domain TypeOf {
function s_Bool_typeof(arg0: s_Bool): Type
function s_Int_i8_typeof(arg0: s_Int_i8): Type
function s_Param_typeof(arg0: s_Param): Type
function s_Fields_typeof(arg0: s_Fields): Type
function s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0_typeof(arg0: s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0): Type
function s_Ref_immutable_typeof(arg0: s_Ref_immutable): Type
function s_UInt_u32_typeof(arg0: s_UInt_u32): Type
}
field p_UInt_u32_val: s_UInt_u32
field p_Int_i8_val: s_Int_i8
field p_Bool_val: s_Bool
field p_Ref_immutable_val: s_Ref_immutable
function f_Fields$colon$$colon$get_field_1(_1p: s_Ref_immutable): s_UInt_u32
{
(let _0_1s_bb0_s0_i0 ==
(_1p) in
(let _0_0s_bb0_s0_i0 ==
(make_concrete_s_Fields(_0_1s_bb0_s0_i0.s_Ref_immutable_1).s_Fields_0) in
_0_0s_bb0_s0_i0))
}
function mir_binop_Ge_u32_u32(arg1: s_UInt_u32, arg2: s_UInt_u32): s_Bool
{
s_Bool_cons(s_UInt_u32_value(arg1) >= s_UInt_u32_value(arg2))
}
function mir_unop_Neg_i8(arg: s_Int_i8): s_Int_i8
{
(s_Int_i8_value(arg) == -128 ? arg : s_Int_i8_cons(-s_Int_i8_value(arg)))
}
function make_generic_s_Bool(self: s_Bool): s_Param
ensures make_concrete_s_Bool(result) == self
function make_concrete_s_Bool(snap: s_Param): s_Bool
ensures make_generic_s_Bool(result) == snap
function make_generic_s_Int_i8(self: s_Int_i8): s_Param
ensures make_concrete_s_Int_i8(result) == self
function make_concrete_s_Int_i8(snap: s_Param): s_Int_i8
ensures make_generic_s_Int_i8(result) == snap
function make_generic_s_Fields(self: s_Fields): s_Param
ensures make_concrete_s_Fields(result) == self
function make_concrete_s_Fields(snap: s_Param): s_Fields
ensures make_generic_s_Fields(result) == snap
function make_generic_s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0(self: s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0,
T: Type): s_Param
ensures make_concrete_s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0(result,
s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0_typeof(self).s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0_typaram_T) ==
self
function make_concrete_s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0(snap: s_Param,
T: Type): s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0
ensures make_generic_s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0(result,
T) ==
snap
function s_UInt_u32_unreachable(): s_UInt_u32
requires false
ensures false
function s_0_Tuple_unreachable(): s_0_Tuple
requires false
ensures false
function s_Fields_unreachable(): s_Fields
requires false
ensures false
function s_Int_i8_unreachable(): s_Int_i8
requires false
ensures false
function s_Param_unreachable(): s_Param
requires false
ensures false
function s_3_Tuple_unreachable(): s_3_Tuple
requires false
ensures false
function s_Tuple_unreachable(): s_Tuple
requires false
ensures false
function s_Bool_unreachable(): s_Bool
requires false
ensures false
function s_Ref_immutable_unreachable(): s_Ref_immutable
requires false
ensures false
function s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0_unreachable(): s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0
requires false
ensures false
function s_1_Tuple_unreachable(): s_1_Tuple
requires false
ensures false
function p_UInt_u32_snap(self: Ref): s_UInt_u32
requires acc(p_UInt_u32(self), write)
{
(unfolding acc(p_UInt_u32(self), write) in self.p_UInt_u32_val)
}
function p_0_Tuple_snap(self: Ref): s_0_Tuple
requires acc(p_0_Tuple(self), write)
{
(unfolding acc(p_0_Tuple(self), write) in s_0_Tuple_cons())
}
function p_Fields_field_0(self: Ref): Ref
ensures (self == null) == (result == null)
function p_Fields_field_1(self: Ref): Ref
ensures (self == null) == (result == null)
function p_Fields_snap(self: Ref): s_Fields
requires acc(p_Fields(self), write)
{
(unfolding acc(p_Fields(self), write) in
s_Fields_cons(p_UInt_u32_snap(p_Fields_field_0(self)), p_0_Tuple_snap(p_Fields_field_1(self))))
}
function p_Int_i8_snap(self: Ref): s_Int_i8
requires acc(p_Int_i8(self), write)
{
(unfolding acc(p_Int_i8(self), write) in self.p_Int_i8_val)
}
function p_Param_snap(self: Ref, T: Type): s_Param
function p_3_Tuple_field_0(self: Ref, T0: Type, T1: Type, T2: Type): Ref
ensures (self == null) == (result == null)
function p_3_Tuple_field_1(self: Ref, T0: Type, T1: Type, T2: Type): Ref
ensures (self == null) == (result == null)
function p_3_Tuple_field_2(self: Ref, T0: Type, T1: Type, T2: Type): Ref
ensures (self == null) == (result == null)
function p_3_Tuple_snap(self: Ref, T0: Type, T1: Type, T2: Type): s_3_Tuple
requires acc(p_3_Tuple(self, T0, T1, T2), write)
{
(unfolding acc(p_3_Tuple(self, T0, T1, T2), write) in
s_3_Tuple_cons(p_Param_snap(p_3_Tuple_field_0(self, T0, T1, T2), T0), p_Param_snap(p_3_Tuple_field_1(self,
T0, T1, T2), T0), p_Param_snap(p_3_Tuple_field_2(self, T0, T1, T2), T0)))
}
function p_Bool_snap(self: Ref): s_Bool
requires acc(p_Bool(self), write)
{
(unfolding acc(p_Bool(self), write) in self.p_Bool_val)
}
function p_Tuple_field_0(self: Ref, T: Type): Ref
ensures (self == null) == (result == null)
function p_Tuple_field_1(self: Ref, T: Type): Ref
ensures (self == null) == (result == null)
function p_Tuple_snap(self: Ref, T: Type): s_Tuple
requires acc(p_Tuple(self, T), write)
{
(unfolding acc(p_Tuple(self, T), write) in
s_Tuple_cons(p_3_Tuple_snap(p_Tuple_field_0(self, T), s_Bool_type(), T,
s_Int_i8_type()), p_Fields_snap(p_Tuple_field_1(self, T))))
}
function p_Ref_immutable_deref(self: Ref, T: Type): Ref
requires acc(p_Ref_immutable(self, T), write)
{
(unfolding acc(p_Ref_immutable(self, T), write) in
self.p_Ref_immutable_val.s_Ref_immutable_0)
}
function p_Ref_immutable_snap(self: Ref, T: Type): s_Ref_immutable
requires acc(p_Ref_immutable(self, T), write)
ensures s_Param_typeof(result.s_Ref_immutable_1) == T
{
(unfolding acc(p_Ref_immutable(self, T), write) in
self.p_Ref_immutable_val)
}
function p_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0_field_0(self: Ref,
T: Type): Ref
ensures (self == null) == (result == null)
function p_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0_snap(self: Ref,
T: Type): s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0
requires acc(p_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0(self,
T), write)
{
(unfolding acc(p_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0(self,
T), write) in
s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0_cons(p_Ref_immutable_snap(p_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0_field_0(self,
T), s_Fields_type())))
}
predicate p_UInt_u32(self: Ref) {
acc(self.p_UInt_u32_val, write)
}
predicate p_0_Tuple(self: Ref) {
true
}
predicate p_Fields(self: Ref) {
acc(p_UInt_u32(p_Fields_field_0(self)), write) &&
acc(p_0_Tuple(p_Fields_field_1(self)), write)
}
predicate p_Int_i8(self: Ref) {
acc(self.p_Int_i8_val, write)
}
predicate p_Param(self: Ref, T: Type)
predicate p_3_Tuple(self: Ref, T0: Type, T1: Type, T2: Type) {
acc(p_Param(p_3_Tuple_field_0(self, T0, T1, T2), T0), write) &&
(acc(p_Param(p_3_Tuple_field_1(self, T0, T1, T2), T0), write) &&
acc(p_Param(p_3_Tuple_field_2(self, T0, T1, T2), T0), write))
}
predicate p_Bool(self: Ref) {
acc(self.p_Bool_val, write)
}
predicate p_Tuple(self: Ref, T: Type) {
acc(p_3_Tuple(p_Tuple_field_0(self, T), s_Bool_type(), T, s_Int_i8_type()), write) &&
acc(p_Fields(p_Tuple_field_1(self, T)), write)
}
predicate p_Ref_immutable(self: Ref, T: Type) {
acc(self.p_Ref_immutable_val, write) &&
s_Param_typeof(self.p_Ref_immutable_val.s_Ref_immutable_1) == T
}
predicate p_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0(self: Ref,
T: Type) {
acc(p_Ref_immutable(p_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0_field_0(self,
T), s_Fields_type()), write)
}
method m_test(_0p: Ref, _1p: Ref, _2p: Ref, T: Type)
requires acc(p_Int_i8(_1p), write)
requires acc(p_Param(_2p, T), write)
requires true
ensures acc(p_Fields(_0p), write)
ensures true
ensures s_Bool_value((let _0_1s_bb0_s0_i0 ==
(old(p_Int_i8_snap(_1p))) in
(let _0_2s_bb0_s0_i0 ==
(old(p_Param_snap(_2p, T))) in
(let _0_3s_bb0_s0_i0 ==
(p_Fields_snap(_0p)) in
(let _0_5s_bb0_s2_i1 ==
(s_0_Tuple_cons()) in
(let _0_9s_bb0_s7_i1 ==
(s_Ref_immutable_cons(null, make_generic_s_Fields(_0_3s_bb0_s0_i0))) in
(let _0_8s_bb0_s8_i1 ==
(s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0_cons(_0_9s_bb0_s7_i1)) in
(let _0_7s_bb0_s10_i1 ==
(s_Ref_immutable_cons(null, make_generic_s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0(_0_8s_bb0_s8_i1,
T))) in
(let _0_6s_bb0_s11_i1 ==
(s_Ref_immutable_cons(null, make_generic_s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0(make_concrete_s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0(_0_7s_bb0_s10_i1.s_Ref_immutable_1,
T), T))) in
(let _0_4s_bb0_s12_i1 ==
(s_Bool_cons((forall qvar_0_0: s_UInt_u32 :: s_Bool_value((let _1_1s_bb0_s0_i0 ==
(_0_6s_bb0_s11_i1) in
(let _1_2s_bb0_s0_i0 ==
(qvar_0_0) in
(let _1_4s_bb0_s2_i1 ==
(_1_2s_bb0_s0_i0) in
(let _1_6s_bb0_s5_i1 ==
(s_Ref_immutable_cons(null, make_generic_s_Fields(make_concrete_s_Fields(make_concrete_s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0(_1_1s_bb0_s0_i0.s_Ref_immutable_1,
T).s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0_0.s_Ref_immutable_1)))) in
(let _1_5s_bb0_s6_i1 ==
(f_Fields$colon$$colon$get_field_1(_1_6s_bb0_s5_i1)) in
(let _1_3s_bb1_s1_i1 ==
(mir_binop_Ge_u32_u32(_1_4s_bb0_s2_i1, _1_5s_bb0_s6_i1)) in
(let _1_phi_bb1_s2_i0 ==
((s_Bool_value(_1_3s_bb1_s1_i1) ==
false ?
(let _1_0s_bb3_s2_i0 ==
(s_Bool_cons(true)) in
s_1_Tuple_cons(make_generic_s_Bool(_1_0s_bb3_s2_i0))) :
(let _1_7s_bb2_s3_i1 ==
(_1_2s_bb0_s0_i0) in
(let _1_8s_bb2_s5_i1 ==
(_1_2s_bb0_s0_i0) in
(let _1_0s_bb2_s6_i1 ==
(mir_binop_Ge_u32_u32(_1_7s_bb2_s3_i1,
_1_8s_bb2_s5_i1)) in
s_1_Tuple_cons(make_generic_s_Bool(_1_0s_bb2_s6_i1))))))) in
(let _1_0s_bb1_s2_i2 ==
(make_concrete_s_Bool(_1_phi_bb1_s2_i0.s_1_Tuple_0)) in
_1_0s_bb1_s2_i2)))))))))))) in
(let _0_0s_bb1_s6_i0 ==
(_0_4s_bb0_s12_i1) in
_0_0s_bb1_s6_i0)))))))))))
{
var _3p: Ref
var _4p: Ref
var _5p: Ref
var _6p: Ref
var _7p: Ref
var _8p: Ref
var _9p: Ref
var _10p: Ref
var _from_bb0_to_bb1: Bool
var _from_bb3_to_bb4: Bool
var _from_bb1_to_bb2: Bool
var _from_bb2_to_bb3: Bool
var _tmp0: s_Param
var _tmp1: s_Int_i8
var _tmp2: s_Param
var _tmp3: s_Int_i8
var _tmp4: s_0_Tuple
var _tmp5: s_3_Tuple
var _tmp6: s_Fields
var _tmp7: s_0_Tuple
label start
// var _3p
// var _4p
// var _5p
// var _6p
// var _7p
// var _8p
// var _9p
// var _10p
_from_bb0_to_bb1 := false
_from_bb3_to_bb4 := false
_from_bb1_to_bb2 := false
_from_bb2_to_bb3 := false
goto bb_0
label bb_0
// [MIR] bb0[0]: StorageLive(_3)
// [MIR] bb0[1]: StorageLive(_4)
// [MIR] bb0[2]: StorageLive(_5)
// [MIR] bb0[3]: _5 = move _2
// (ignoring)
// (ignoring)
// (ignoring)
// (ignoring)
// (ignoring)
// var _tmp0
_tmp0 := p_Param_snap(_2p, T)
exhale acc(p_Param(_2p, T), write)
p_Param_assign(_5p, T, _tmp0)
label _after_0_3
// [MIR] bb0[4]: StorageLive(_6)
// [MIR] bb0[5]: StorageLive(_7)
// [MIR] bb0[6]: _7 = copy _1
// (ignoring)
// (ignoring)
// (ignoring)
p_Int_i8_assign(_7p, p_Int_i8_snap(_1p))
label _after_0_6
// [MIR] bb0[7]: _6 = Neg(move _7)
// (ignoring)
// (ignoring)
// (ignoring)
// (ignoring)
// (ignoring)
// var _tmp1
_tmp1 := p_Int_i8_snap(_7p)
exhale acc(p_Int_i8(_7p), write)
p_Int_i8_assign(_6p, mir_unop_Neg_i8(_tmp1))
label _after_0_7
// [MIR] bb0[8]: StorageDead(_7)
// (ignoring)
// [MIR] bb0[9]: _4 = (const true, move _5, move _6)
// (ignoring)
// (ignoring)
// (ignoring)
// (ignoring)
// (ignoring)
// (ignoring)
// (ignoring)
// var _tmp2
_tmp2 := p_Param_snap(_5p, T)
exhale acc(p_Param(_5p, T), write)
// var _tmp3
_tmp3 := p_Int_i8_snap(_6p)
exhale acc(p_Int_i8(_6p), write)
p_3_Tuple_assign(_4p, s_Bool_type(), T, s_Int_i8_type(), s_3_Tuple_cons(make_generic_s_Bool(s_Bool_cons(true)), _tmp2, make_generic_s_Int_i8(_tmp3)))
label _after_0_9
// [MIR] bb0[10]: StorageDead(_6)
// (ignoring)
// [MIR] bb0[11]: drop(_5) -> [return: bb1, unwind: bb5]
// PCG (T) pre_operands
// PCG (T) post_operands
// PCG (T) pre_main
// (ignoring)
// (ignoring)
// PCG (T) post_main
_from_bb0_to_bb1 := true
label _after_0_11
goto bb_1
label bb_1
// [MIR] bb1[0]: StorageDead(_5)
// (ignoring)
// [MIR] bb1[1]: StorageLive(_8)
// [MIR] bb1[2]: StorageLive(_9)
// [MIR] bb1[3]: _9 = ()
// (ignoring)
// (ignoring)
// (ignoring)
p_0_Tuple_assign(_9p, s_0_Tuple_cons())
label _after_1_3
// [MIR] bb1[4]: _8 = Fields { field_1: const 0_u32, field_2: move _9 }
// (ignoring)
// (ignoring)
// (ignoring)
// (ignoring)
// (ignoring)
// var _tmp4
_tmp4 := p_0_Tuple_snap(_9p)
exhale acc(p_0_Tuple(_9p), write)
p_Fields_assign(_8p, s_Fields_cons(s_UInt_u32_cons(0), _tmp4))
label _after_1_4
// [MIR] bb1[5]: StorageDead(_9)
// (ignoring)
// [MIR] bb1[6]: _3 = Tuple::<T>(move _4, move _8)
// (ignoring)
// (ignoring)
// (ignoring)
// (ignoring)
// (ignoring)
// (ignoring)
// (ignoring)
// var _tmp5
_tmp5 := p_3_Tuple_snap(_4p, s_Bool_type(), T, s_Int_i8_type())
exhale acc(p_3_Tuple(_4p, s_Bool_type(), T, s_Int_i8_type()), write)
// var _tmp6
_tmp6 := p_Fields_snap(_8p)
exhale acc(p_Fields(_8p), write)
p_Tuple_assign(_3p, T, s_Tuple_cons(_tmp5, _tmp6))
label _after_1_6
// [MIR] bb1[7]: StorageDead(_8)
// (ignoring)
// [MIR] bb1[8]: drop(_4) -> [return: bb2, unwind: bb6]
// PCG (T) pre_operands
// PCG (T) post_operands
// PCG (T) pre_main
// (ignoring)
// (ignoring)
// PCG (T) post_main
_from_bb1_to_bb2 := true
label _after_1_8
goto bb_2
label bb_2
// [MIR] bb2[0]: StorageDead(_4)
// (ignoring)
// [MIR] bb2[1]: FakeRead(ForLet(None), _3)
label _after_2_1
// [MIR] bb2[2]: StorageLive(_10)
// [MIR] bb2[3]: _10 = ()
// (ignoring)
// (ignoring)
// (ignoring)
p_0_Tuple_assign(_10p, s_0_Tuple_cons())
label _after_2_3
// [MIR] bb2[4]: _0 = Fields { field_1: const 0_u32, field_2: move _10 }
// (ignoring)
// (ignoring)
// (ignoring)
// (ignoring)
// (ignoring)
// var _tmp7
_tmp7 := p_0_Tuple_snap(_10p)
exhale acc(p_0_Tuple(_10p), write)
p_Fields_assign(_0p, s_Fields_cons(s_UInt_u32_cons(0), _tmp7))
label _after_2_4
// [MIR] bb2[5]: StorageDead(_10)
// (ignoring)
// [MIR] bb2[6]: drop(_3) -> [return: bb3, unwind: bb6]
// PCG (T) pre_operands
// PCG (T) post_operands
// PCG (T) pre_main
// (ignoring)
// (ignoring)
// PCG (T) post_main
_from_bb2_to_bb3 := true
label _after_2_6
goto bb_3
label bb_3
// [MIR] bb3[0]: StorageDead(_3)
// (ignoring)
// [MIR] bb3[1]: drop(_2) -> [return: bb4, unwind: bb7]
// PCG (T) pre_operands
// PCG (T) post_operands
// PCG (T) pre_main
// (ignoring)
// (ignoring)
// PCG (T) post_main
_from_bb3_to_bb4 := true
label _after_3_1
goto bb_4
label bb_4
// [MIR] bb4[0]: return
// PCG (T) pre_operands
// PCG (T) post_operands
// PCG (T) pre_main
// PCG (T) post_main
label package_post0
label _after_4_0
goto end
label bb_5
// cleanup block
assert false
label bb_6
// cleanup block
assert false
label bb_7
// cleanup block
assert false
label end
// return
}
method make_generic_p_Bool(self: Ref)
requires acc(p_Bool(self), write)
ensures acc(p_Param(self, s_Bool_type()), write)
ensures old(make_generic_s_Bool(p_Bool_snap(self))) ==
p_Param_snap(self, s_Bool_type())
method make_concrete_p_Bool(self: Ref)
requires acc(p_Param(self, s_Bool_type()), write)
ensures acc(p_Bool(self), write)
ensures old(p_Param_snap(self, s_Bool_type())) ==
make_generic_s_Bool(p_Bool_snap(self))
method make_generic_p_Int_i8(self: Ref)
requires acc(p_Int_i8(self), write)
ensures acc(p_Param(self, s_Int_i8_type()), write)
ensures old(make_generic_s_Int_i8(p_Int_i8_snap(self))) ==
p_Param_snap(self, s_Int_i8_type())
method make_concrete_p_Int_i8(self: Ref)
requires acc(p_Param(self, s_Int_i8_type()), write)
ensures acc(p_Int_i8(self), write)
ensures old(p_Param_snap(self, s_Int_i8_type())) ==
make_generic_s_Int_i8(p_Int_i8_snap(self))
method make_generic_p_Fields(self: Ref)
requires acc(p_Fields(self), write)
ensures acc(p_Param(self, s_Fields_type()), write)
ensures old(make_generic_s_Fields(p_Fields_snap(self))) ==
p_Param_snap(self, s_Fields_type())
method make_concrete_p_Fields(self: Ref)
requires acc(p_Param(self, s_Fields_type()), write)
ensures acc(p_Fields(self), write)
ensures old(p_Param_snap(self, s_Fields_type())) ==
make_generic_s_Fields(p_Fields_snap(self))
method p_UInt_u32_assign(self: Ref, value: s_UInt_u32)
ensures acc(p_UInt_u32(self), write)
ensures p_UInt_u32_snap(self) == value
method p_0_Tuple_assign(self: Ref, value: s_0_Tuple)
ensures acc(p_0_Tuple(self), write)
ensures p_0_Tuple_snap(self) == value
method p_Fields_assign(self: Ref, value: s_Fields)
ensures acc(p_Fields(self), write)
ensures p_Fields_snap(self) == value
method p_Int_i8_assign(self: Ref, value: s_Int_i8)
ensures acc(p_Int_i8(self), write)
ensures p_Int_i8_snap(self) == value
method p_Param_assign(self: Ref, T: Type, value: s_Param)
ensures acc(p_Param(self, T), write)
ensures p_Param_snap(self, T) == value
method p_3_Tuple_assign(self: Ref, T0: Type, T1: Type, T2: Type, value: s_3_Tuple)
ensures acc(p_3_Tuple(self, T0, T1, T2), write)
ensures p_3_Tuple_snap(self, T0, T1, T2) == value
method p_Bool_assign(self: Ref, value: s_Bool)
ensures acc(p_Bool(self), write)
ensures p_Bool_snap(self) == value
method p_Tuple_assign(self: Ref, T: Type, value: s_Tuple)
ensures acc(p_Tuple(self, T), write)
ensures p_Tuple_snap(self, T) == value
method p_Ref_immutable_assign(self: Ref, T: Type, value: s_Ref_immutable)
ensures acc(p_Ref_immutable(self, T), write)
ensures p_Ref_immutable_snap(self, T) == value
method p_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0_assign(self: Ref,
T: Type, value: s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0)
ensures acc(p_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0(self,
T), write)
ensures p_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0_snap(self,
T) ==
value
adt s_0_Tuple {
s_0_Tuple_cons()
}
adt s_Fields {
s_Fields_cons(s_Fields_0: s_UInt_u32, s_Fields_1: s_0_Tuple)
}
adt s_3_Tuple {
s_3_Tuple_cons(s_3_Tuple_0: s_Param, s_3_Tuple_1: s_Param, s_3_Tuple_2: s_Param)
}
adt s_Tuple {
s_Tuple_cons(s_Tuple_0: s_3_Tuple, s_Tuple_1: s_Fields)
}
adt s_Ref_immutable {
s_Ref_immutable_cons(s_Ref_immutable_0: Ref, s_Ref_immutable_1: s_Param)
}
adt s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0 {
s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0_cons(s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0_0: s_Ref_immutable)
}
adt s_1_Tuple {
s_1_Tuple_cons(s_1_Tuple_0: s_Param)
}
adt Type {
s_Bool_type()
s_Int_i8_type()
s_Fields_type()
s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0_type(s_prusti_post_item_test_3bb22df32a5a482fa3eacc11be0995f6_Closure_0_typaram_T: Type)
s_Ref_immutable_type(s_Ref_immutable_typaram_T: Type)
s_UInt_u32_type()
Unknown_type(non_unit: Int)
}
