New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Minimal support for execution of a parsed program #415

Open

jberthold opened this issue Sep 4, 2024 · 0 comments

Member

jberthold commented Sep 4, 2024 •

edited by gtrepta

Loading

Given a pretty minimal true.rs:

fn test_true() -> bool {
  true
}

What needs to be done?

User calls koat true.rs from CLI
The stable MIR json gets generated from the source file
The needed information (blue graph?) from the JSON is loaded into the initial K configuration
A claim with the proper requires/ensures clauses gets generated from the config
The claim gets symbolically executed
Relevant information from the execution result is gathered and reported to the user

The text was updated successfully, but these errors were encountered:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment