Module property_checker 

Unified property checker for the symbolic VM.

PropertyChecker::check is the entry point; check_inner dispatches each PropertyKind to a per-family check_* method living in one of the sibling submodules (memory, bounds, typed, numeric, string, alias, cstr, transmute). Shared helpers live in util.

Modules

alias 🔒

bounds 🔒

cstr 🔒

ValidCStr property checking for the symbolic VM.

memory 🔒

numeric 🔒

string 🔒

transmute 🔒

Transmute / trait / size property checking for the symbolic VM.

typed 🔒

util 🔒

Structs

PropertyChecker

Functions

signature_return_has_lifetime 🔒

Check if the source-level function signature has a named lifetime in return type.

utf8_validity 🔒

Build the boolean expression “bytes form a valid UTF-8 sequence”.