Skip to content

Typestate apparently doesn't handle loops... #819

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

Closed
eholk opened this issue Aug 13, 2011 · 1 comment
Closed

Typestate apparently doesn't handle loops... #819

eholk opened this issue Aug 13, 2011 · 1 comment

Comments

@eholk
Copy link
Contributor

eholk commented Aug 13, 2011

fn test00_start(ch: _chan[int], message: int, count: int) {
    log "Starting test00_start";
    let i: int = 0;
    while i < count {
        log "Sending Message";
        send(ch, message);
        i = i + 1;
    }
    log "Ending test00_start";
}

send uses move-mode for the second argument, which means that message is deinitialized the second time through the loop. Typestate should catch this.

@ghost ghost assigned catamorphism Aug 13, 2011
catamorphism added a commit that referenced this issue Aug 18, 2011
Add the infrastructure for arguments -- as well as local vars --
to be deinitialized with move-mode calls. Address Issue #819
@catamorphism
Copy link
Contributor

Actually, loops don't have anything to do with it. Typestate didn't handle move-mode arguments correctly at all. Just pushed a commit that fixes it.

keeperofdakeys pushed a commit to keeperofdakeys/rust that referenced this issue Dec 12, 2017
Bump to 0.2.33

Just bumping the release to make getprotobyname, getprotobynumber and getservbyname available.
ZuseZ4 added a commit to EnzymeAD/rust that referenced this issue Mar 7, 2023
* Fix shuffle canonicalization

* Add assertion

Co-authored-by: Manuel Drehwald <git@manuel.drehwald.info>
celinval pushed a commit to celinval/rust-dev that referenced this issue Jun 4, 2024
* Compute hash for test runs based on main files

* Look up `src` instead of `kani-compiler`

* Check changes in library folder
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

2 participants