formal-land / coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦
GNU Affero General Public License v3.0
418 stars 14 forks source link

`verify_instr` simulation #590

Closed InfiniteEchoes closed 2 months ago

InfiniteEchoes commented 2 months ago

After #587 , pretty much of the dependencies have been resolved nicely.

This PR is focusing on the main task: #575 .

This PR:

Known Issues

In current implementation, we ignore any messages for PartialVMError for simplicity

InfiniteEchoes commented 2 months ago

I'm done with everything that I need to do.