Expand description
Builtin call models: API behaviour modelling when MIR is unavailable.
Each recognised standard-library API is described by a single table
row: a matcher (from crate::verify::api_classify) and an
effect builder. lookup_effect scans the table linearly (first match
wins) and converts the matched row into the effect summary consumed by the
VM; is_modeled reports whether a call is in the table (used by the path
graph to keep modelled calls opaque instead of inlining their branchy CFG).
Two layers:
- Matchers —
crate::verify::api_classifyDefIdclassifiers. - Effect functions — produce the
Vec<CallEffect>for a single API.
Macros§
- ED 🔒
DefId-based matcher row (fn(Option<DefId>) -> bool).
Structs§
Enums§
Statics§
- REGISTRY 🔒
Functions§
- dest_
is_ 🔒pointer - eff_
alias_ 🔒arg0 - eff_
alias_ 🔒ptr - eff_
align_ 🔒offset - eff_
align_ 🔒to - eff_
box_ 🔒alloc - eff_
box_ 🔒from_ vec - eff_
cmp_ 🔒min - eff_
drop_ 🔒memory - eff_
exchange_ 🔒malloc - eff_
from_ 🔒raw_ parts - eff_
layout_ 🔒align - eff_
layout_ 🔒const - eff_len 🔒
- eff_
mem_ 🔒replace - eff_
new_ 🔒allocation - eff_
new_ 🔒allocation_ from_ cap - eff_
new_ 🔒unchecked NonNull::new_unchecked(ptr): a transparent re-wrap that preservesptr’s value and provenance (element offset included), inheriting non-nullness from the source rather than asserting it.- eff_
none 🔒 - eff_
option_ 🔒scan_ index - eff_
overflowing_ 🔒nz - eff_
ownership_ 🔒recon - eff_
ptr_ 🔒add - eff_
ptr_ 🔒add_ byte - eff_
ptr_ 🔒arith - Shared model for
ReturnPointerAdd/ReturnPointerSub. - eff_
ptr_ 🔒sub - eff_
ptr_ 🔒sub_ byte - eff_
return_ 🔒abs - eff_
return_ 🔒add - eff_
return_ 🔒clamp - eff_
return_ 🔒max - eff_
return_ 🔒mul - eff_
return_ 🔒neg - eff_
return_ 🔒nonzero_ iff - eff_
return_ 🔒option_ some_ add - eff_
return_ 🔒option_ some_ mul - eff_
return_ 🔒option_ some_ nonzero - eff_
return_ 🔒option_ some_ nonzero_ iff - eff_
scan_ 🔒length - eff_
select_ 🔒unpredictable - eff_
slice_ 🔒range - eff_
sliceindex_ 🔒get_ unchecked SliceIndex::get_unchecked(self, slice)/get_unchecked_mut: returns an element pointer atslice + self(receiver is the index, slice pointer is argument 1). Element-strided add off argument 1, inheriting non-nullness from the slice.- eff_
split_ 🔒at - eff_
vec_ 🔒from_ box - eff_
write_ 🔒mem - is_
modeled 🔒 - True when
calleematches a hand-modelled API in the registry. The path graph uses this to keep such calls opaque (it must not inline their branchy CFG when the VM models their semantics more precisely). - layout_
call_ 🔒ty - layout_
constant_ 🔒effect - lookup_
effect 🔒