A symbolic execution tool for Move, which is a smart contract language designed for Diem.
Clone Diem to the parent directory of Movable. The directory structure should look like:
|_ diem
|_ Movable
Diem repository should be checkout to tag diem-framework-v1.2.0. Other versions are untested.
cargo run <BYTECODE_FILE> -f <FUNCTION_NAME>- Transaction configuration
- Symbolic execution configuration
- Start from states other than genesis
- Symbolic writeset
- Custom data store
- Vector bound check (in plugin or not?)
- Native function modelling
- Stdlib test
- More benchmarks
- Docking with plugin system (intarith plugin running)
- Gas infrastructure
- Debug and log infrastructure
- Single instruction listening support (intarith plugin added)
- Verification plugin support