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

mutability is not inherited through fixed-length vectors #3226

Closed
nikomatsakis opened this issue Aug 20, 2012 · 0 comments
Closed

mutability is not inherited through fixed-length vectors #3226

nikomatsakis opened this issue Aug 20, 2012 · 0 comments
Labels
A-lifetimes Area: Lifetimes / regions A-type-system Area: Type system E-easy Call for participation: Easy difficulty. Experience needed to fix: Not much. Good first issue.
Milestone

Comments

@nikomatsakis
Copy link
Contributor

The following program:

type two_ints = [int * 2];

fn main() {
    let mut foo: two_ints = [0, 1];
    foo[0] = foo[1];
}

erroneously yields:

/Users/nmatsakis/tmp/foo.rs:5:4: 5:9 error: assigning to immutable vec content
/Users/nmatsakis/tmp/foo.rs:5     foo[0] = foo[1];
                                  ^~~~~
error: aborting due to previous error

Note that using a ~[] vec compiles successfully.

RalfJung pushed a commit to RalfJung/rust that referenced this issue Dec 17, 2023
jaisnan added a commit to jaisnan/rust-dev that referenced this issue Jul 29, 2024
While at it, I also added a `--skip-libs` to skip rebuilding the Kani
libraries and standard library at every `cargo build-dev` execution.

We usually only need to rebuild the libraries when we make changes to
them or when we update the Rust toolchain. Rebuilding them can be quite
time consuming when you are making changes to Kani.

Towards rust-lang#3226 rust-lang#3153

Co-authored-by: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com>
jaisnan pushed a commit to jaisnan/rust-dev that referenced this issue Jul 29, 2024
This subcommand will take the path to the standard library.
   
It will then use `cargo build -Z build-std` to build the custom standard
library and verify any harness found during the build.

## Call out

- So far I only performed manual tests. I'm going to add a few unit
tests and a script in the next revision.

Resolves rust-lang#3226 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
jaisnan pushed a commit to jaisnan/rust-dev that referenced this issue Jul 29, 2024
In rust-lang#3226, we added a new command that allow Kani to verify properties in
a custom standard library. In this PR, we create a script test that
create a modified version of the standard library and runs Kani against
it.

I also moved the script based tests to run after the more generic
regression jobs. I think the script jobs are a bit harder to debug, they
may take longer, and they are usually very specific to a few features.
So probably best if we run the more generic tests first.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-lifetimes Area: Lifetimes / regions A-type-system Area: Type system E-easy Call for participation: Easy difficulty. Experience needed to fix: Not much. Good first issue.
Projects
None yet
Development

No branches or pull requests

1 participant