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

Teach typechecker that uint is <plusable>. #88

Closed
froystig opened this issue Jun 28, 2010 · 1 comment
Closed

Teach typechecker that uint is <plusable>. #88

froystig opened this issue Jun 28, 2010 · 1 comment
Labels
A-type-system Area: Type system E-easy Call for participation: Easy difficulty. Experience needed to fix: Not much. Good first issue.

Comments

@froystig
Copy link
Contributor

At the moment,

fn main() {
  let uint i = uint(1);
  i += uint(1);
}

fails to compile, giving the error:

uintplus.rs:3:2 - 4:0:E:Error: mismatched types: uint vs. <plusable>

Fix this.

@froystig
Copy link
Contributor Author

Teach the typechecker that uints are integral types. Closed by 66d313d.

oli-obk pushed a commit to oli-obk/rust that referenced this issue Jul 19, 2017
keeperofdakeys pushed a commit to keeperofdakeys/rust that referenced this issue Dec 12, 2017
kazcw pushed a commit to kazcw/rust that referenced this issue Oct 23, 2018
* Add _mm_sfence

* Add _mm_getcsr/_mm_setcsr and convenience wrappers

* Use test::black_box to simplify tests

* Use uppercase naming for C-macro equivalents

Discussed at rust-lang/stdarch#84
dlrobertson pushed a commit to dlrobertson/rust that referenced this issue Nov 29, 2018
eddyb pushed a commit to eddyb/rust that referenced this issue Jun 30, 2020
Port to the 2018 edition and cargo-semver cleanups
djtech-dev pushed a commit to djtech-dev/rust that referenced this issue Dec 9, 2021
Derive Clone, Copy, and Hash for BasicBlock
celinval pushed a commit to celinval/rust-dev that referenced this issue Jun 4, 2024
…ng#88)

* Complete and replace the unsized pointer cast implementation

* Respond to code review of unsized pointer cast implementation

Co-authored-by: Mark R. Tuttle <[email protected]>
jaisnan pushed a commit to jaisnan/rust-dev that referenced this issue Oct 15, 2024
…d` (rust-lang#88)

Towards model-checking#53
### Changes

- added contract and harness for `non_null::new`
- added contract and harness for `non_null::new_unchecked`

The difference between the two APIs is that `non_null::new` can handle
null pointers while `non_null::new_unchecked` does not. Therefore the
contract for `non_null::new` does not require a `nonnull` pointer.

### Re-validation
To re-validate the verification results, run `kani verify-std -Z
unstable-options "path/to/library" -Z function-contracts -Z
mem-predicates --harness ptr::non_null::verify::non_null_check_new`.
This will run both harnesses. All default checks should pass.

---------

Co-authored-by: OwO <[email protected]>
Co-authored-by: Zyad Hassan <[email protected]>
This issue was closed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
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