Skip to content
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.

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

Print meaningful error messages with code location #54

Closed
sonmarcho opened this issue Dec 20, 2023 · 1 comment
Closed

Print meaningful error messages with code location #54

sonmarcho opened this issue Dec 20, 2023 · 1 comment

Comments

@sonmarcho
Copy link
Member

For now, whenever Aeneas encounters an error it simply crashes. It would be better to print an error message indicating the reason behind the error and most importantly the part of the code which triggered it.

A first step might simply be to print the file name and the location inside the file.

We also want to be able to run Aeneas in two modes, like Charon:

  • do not abort on failure, go as far as possible and eventually generate definitions with holes while reporting errors (better for the user)
  • abort on the first error (better for debugging)

Later we might want to have a Rust executable which links itself to the Rust compiler, runs Charon then Aeneas and reports all the error messages in the same session.

@sonmarcho
Copy link
Member Author

Mostly solved by #95

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant