This is the source code of KRust, an executable semantics of a subset of Rust using K framework.
Requirements
- Make sure you have installed K framework 4.0.0 successfully. If not, download it here and follow the installation instructions.
- KRust can be successfully run on OS X EI Capitan 10.11.6 and Ubuntu 12.04.5. Other systems with K framework 4.0.0 should run it successfully too.
Download
source code
Usage
Above all, kompile the source code using command:
kompile rs.k
Use krun command to run test cases. For instance:
kun tests/while.rs
Project Structure
- rs-semantics-*.k contains the specific semantics rules.
- rs-syntax.k only defines the syntax.
- rs.k wraps rs-semantics-*.k and rs-syntax.k
- tests includes some Rust codes used to test all the rules. It also contains a folder called passed-files-from-run-pass. The codes in this folder are from Rust compiler’s test suite which krust can also successfully pass. The proofs folder in tests is used for verification.
- extended-float.k is used to implement float numbers.
License
See LICENSE