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

non-mut local variable checking should use typestate #1940

Closed
nikomatsakis opened this issue Mar 7, 2012 · 3 comments
Closed

non-mut local variable checking should use typestate #1940

nikomatsakis opened this issue Mar 7, 2012 · 3 comments
Labels
C-enhancement Category: An issue proposing an enhancement or a PR with one.

Comments

@nikomatsakis
Copy link
Contributor

Right now, I have a simple rule that non-mutable local variables cannot be assigned ever. This is too simplistic. We should track an uninit predicate for each local variable and only allow assignment to x if uninit(x) holds. (Note that it is possible to be in a state where neither init(x) nor uninit(x) holds, if x is initialized on some paths but not others)

I tried delving into the type state module to make these changes but they proved somewhat invasive. Currently predicates are indexed by def_id, for example, but this will have to change as there would be multiple predicates associated with the def_id of each local variable. So I decided to just leave my simple-minded check and file an issue.
@nikomatsakis
Copy link
Contributor Author

(This relates to #1273)

@ghost ghost assigned catamorphism Mar 7, 2012
@nikomatsakis
Copy link
Contributor Author

This applies to the checking of field initialization in ctors as well.

@nikomatsakis
Copy link
Contributor Author

with the new liveness stuff, this is fixed.

@crumblingstatue crumblingstatue mentioned this issue Aug 9, 2017
Closed
3 tasks
celinval added a commit to celinval/rust-dev that referenced this issue Jun 4, 2024
@celinval
Introduce ArtifactType and a few more info to HarnessMetadata (rust-l…
886618c 
…ang#1940)

This is the first change I'm planning to make to allow us to stop linking all *out files together and to introduce per-harness artifact generation in the compiler.

I added the ArtifactType to create a standard way to handle file extensions in different parts of Kani.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
C-enhancement Category: An issue proposing an enhancement or a PR with one.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@nikomatsakis @catamorphism