Simple MIPS-Why3k model
- RegFile register-file model, (read/write operations and predicates for content and preservation),
- arithmetic instructions (already here you will be able to verify your first why3k assembly program),
- the stack memory model and data memory operations (load/store operations with predicates for alignment, content and preservation.
- MIPS ABI (calling convention) and predicates for well-formedness and stack access separation
Arithmetic Instructions
Stack Memory Model
MIPS ABI