Skip to content

Commit 52372f4

Browse files
committed
adjust the function name to real spl-token program
1 parent 86197c8 commit 52372f4

File tree

1 file changed

+9
-0
lines changed

1 file changed

+9
-0
lines changed

kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -55,9 +55,12 @@ module KMIR-SPL-TOKEN
5555
5656
rule #isSPLBorrowFunc("std::cell::RefCell::<std::vec::Vec<u8>>::borrow") => true
5757
rule #isSPLBorrowFunc("std::cell::RefCell::<std::vec::Vec<u8>>::borrow_mut") => true
58+
rule #isSPLBorrowFunc("std::cell::RefCell::<&mut [u8]>::borrow") => true
59+
rule #isSPLBorrowFunc("std::cell::RefCell::<&mut [u8]>::borrow_mut") => true
5860
rule #isSPLBorrowFunc(_) => false [owise]
5961
6062
rule #isSPLBorrowMutFunc("std::cell::RefCell::<std::vec::Vec<u8>>::borrow_mut") => true
63+
rule #isSPLBorrowMutFunc("std::cell::RefCell::<&mut [u8]>::borrow_mut") => true
6164
rule #isSPLBorrowMutFunc(_) => false [owise]
6265
6366
rule #isSPLVecSliceFunc("std::vec::Vec::<u8>::as_slice") => true
@@ -67,9 +70,13 @@ module KMIR-SPL-TOKEN
6770
rule #isSPLVecSliceFunc("<std::vec::Vec<u8> as std::ops::IndexMut<std::ops::RangeFull>>::index_mut") => true
6871
rule #isSPLVecSliceFunc(_) => false [owise]
6972
73+
7074
rule #isSPLRefDerefFunc("<std::cell::Ref<'_, std::vec::Vec<u8>> as std::ops::Deref>::deref") => true
7175
rule #isSPLRefDerefFunc("<std::cell::RefMut<'_, std::vec::Vec<u8>> as std::ops::Deref>::deref") => true
7276
rule #isSPLRefDerefFunc("<std::cell::RefMut<'_, std::vec::Vec<u8>> as std::ops::DerefMut>::deref_mut") => true
77+
rule #isSPLRefDerefFunc("<std::cell::Ref<'_, &mut [u8]> as std::ops::Deref>::deref") => true
78+
rule #isSPLRefDerefFunc("<std::cell::RefMut<'_, &mut [u8]> as std::ops::Deref>::deref") => true
79+
rule #isSPLRefDerefFunc("<std::cell::RefMut<'_, &mut [u8]> as std::ops::DerefMut>::deref_mut") => true
7380
rule #isSPLRefDerefFunc("<core::cell::RefMut<'_, alloc::vec::Vec<u8>> as core::ops::DerefMut>::deref_mut") => true
7481
rule #isSPLRefDerefFunc("<std::cell::RefMut<'_, alloc::vec::Vec<u8>> as std::ops::DerefMut>::deref_mut") => true
7582
rule #isSPLRefDerefFunc("<core::cell::RefMut<'_, std::vec::Vec<u8>> as core::ops::DerefMut>::deref_mut") => true
@@ -163,6 +170,8 @@ expose the wrapped payload directly.
163170
</k>
164171
requires #functionName(lookupFunction(#tyOfCall(FUNC)))
165172
==String "<std::rc::Rc<std::cell::RefCell<std::vec::Vec<u8>>> as std::ops::Deref>::deref"
173+
orBool #functionName(lookupFunction(#tyOfCall(FUNC)))
174+
==String "<std::rc::Rc<std::cell::RefCell<&mut [u8]>> as std::ops::Deref>::deref"
166175
[priority(30), preserves-definedness]
167176
168177
syntax KItem ::= #finishSPLRcDeref ( Evaluation , Place , MaybeBasicBlockIdx , Operand , Operands , UnwindAction ) [seqstrict(1)]

0 commit comments

Comments
 (0)