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.

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

Introduce rmctool attribute validation #689

Closed
2 of 3 tasks
tedinski opened this issue Dec 10, 2021 · 0 comments · Fixed by #2132
Closed
2 of 3 tasks

Introduce rmctool attribute validation #689

tedinski opened this issue Dec 10, 2021 · 0 comments · Fixed by #2132
Assignees
@celinval @jaisnan
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.

Comments

@tedinski
Copy link
Contributor

tedinski commented Dec 10, 2021 •
edited
Loading

We presently do not do any validation of rmctool attributes in the rmc compiler.

Presently, we only have rmctool::proof, so the only real missing validations are:

  • Check to ensure there aren't multiple proof attributes on the function.
  • Check there's no parameters to proof (#[rmc::proof(stuff, here)])
  • Check the function being annotated to ensure it has no parameters. (Initially: in the future, we might try to handle parameters as nondet. But this is something to design to handle the assumptions problem...)

When we add more attributes, those need validation too.

Possibly we should do this at the proc_macro level, instead of in the rmc backend of the compiler?
@tedinski tedinski added the [C] Bug This is a bug. Something isn't working. label Dec 10, 2021
@tedinski tedinski mentioned this issue Dec 10, 2021
Merged
4 tasks
@jaisnan jaisnan self-assigned this Feb 23, 2022
@jaisnan jaisnan mentioned this issue Mar 1, 2022
Merged
4 tasks
@zhassan-aws zhassan-aws added Cat: enhancement and removed [C] Bug This is a bug. Something isn't working. labels Mar 16, 2022
@celinval celinval added [C] Feature / Enhancement A new feature request or enhancement to an existing feature. and removed Cat: enhancement labels Nov 9, 2022
@tedinski tedinski mentioned this issue Jan 17, 2023
Closed
@celinval celinval self-assigned this Jan 17, 2023
celinval added a commit to celinval/kani-dev that referenced this issue Jan 17, 2023
@celinval
Improve #[kani::proof] handling
6fa684a 
- Change `#[kani::proof]` expansion so it doesn't include `#[no_mangle]`
but includes `[allow(dead_code)]`. Fixes model-checking#661 and fixes model-checking#689.

- Add a check for harnesses with arguments and merge the checks into one
  function. Fixes model-checking#1919
@celinval celinval mentioned this issue Jan 17, 2023
Merged
4 tasks
celinval added a commit that referenced this issue Jan 19, 2023
@celinval @zhassan-aws
Reject proof harnesses with arguments (#2132)
0eb1fe8 
- Change `#[kani::proof]` expansion so it doesn't include `#[no_mangle]` but includes `[allow(dead_code)]`. (#661 and #689).

- Add a check for harnesses with arguments and merge the checks into one function (#1919). 

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@celinval celinval

@jaisnan jaisnan

Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.
Projects
No open projects
Kani 2023-01-23
Status: Done
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Reject proof harnesses with arguments celinval/kani-dev
4 participants
@tedinski @celinval @zhassan-aws @jaisnan