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

Unique boxes containing pinned kinds should be shared kinds #977

Closed
brson opened this issue Sep 25, 2011 · 3 comments
Closed

Unique boxes containing pinned kinds should be shared kinds #977

brson opened this issue Sep 25, 2011 · 3 comments
Labels
A-type-system Area: Type system

Comments

@brson
Copy link
Contributor

brson commented Sep 25, 2011

Currently unique boxes containing pinned kinds are pinned kinds but Graydon says they are supposed to be shared. To make this change we have to make sure that unique boxes containing pinned kinds can't be copied. I don't fully understand yet.
@ghost ghost assigned brson Sep 25, 2011
@brson
Copy link
Contributor Author

brson commented Sep 26, 2011

Same is true for vectors of pinned

@brson brson closed this as completed in 223f5be Sep 26, 2011
@brson brson reopened this Sep 27, 2011
@brson
Copy link
Contributor Author

brson commented Sep 27, 2011

I reverted this at least temporarily. Currently no unique kinds raise pinned to shared because that makes copying rules very complicated. So I'm trying to make sure that resources can't be copied first, then once there are lots of working tests we can try to make them embeddable in uniques.

@marijnh
Copy link
Contributor

marijnh commented Nov 15, 2011

This seems like a bad idea, and is (if I understand the reasoning behind it) better handled by the revised kind system.

@marijnh marijnh closed this as completed Nov 15, 2011
bors pushed a commit to rust-lang-ci/rust that referenced this issue Oct 26, 2020
@bjorn3
Some changes necessary for Windows support
daad966 
cc rust-lang#977
ZuseZ4 pushed a commit to EnzymeAD/rust that referenced this issue Mar 7, 2023
@wsmoses
Fix pgcstack bug (rust-lang#977)
5d1e000
coastalwhite pushed a commit to coastalwhite/rust that referenced this issue Aug 5, 2023
@minybot
Avx512vbmi (rust-lang#977)
0000457
celinval added a commit to celinval/rust-dev that referenced this issue Jun 4, 2024
@celinval @tedinski
Fix config argument precedence and handling of CBMC options. (rust-la…
28bd56e 
…ng#977)

Cargo kani wouldn't work if the project Cargo.toml had --cbmc-args and
if the command line also included --cbmc-args.

The other issue is that the options in the project configuration had
precedence over the ones from the command line, which is misleading.
For example, if the Cargo.toml had a harness function defined to run by
default, the user would still run the default harness even if they ran:

```
cargo kani --function <different_harness>
```
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
A-type-system Area: Type system
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@marijnh @brson