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

strings in pattern-alt statements #53

Closed
graydon opened this issue Jun 22, 2010 · 1 comment
Closed

strings in pattern-alt statements #53

graydon opened this issue Jun 22, 2010 · 1 comment
Labels
A-frontend Area: Compiler frontend (errors, parsing and HIR)

Comments

@graydon
Copy link
Contributor

graydon commented Jun 22, 2010

Pattern-alts don't match on literal strings at the moment. This may be good to support.

@graydon
Copy link
Contributor Author

graydon commented Jan 27, 2011

Shifted to rustc. Version in rustboot not required for bootstrapping.

@brson brson closed this as completed in 7105cd1 Jun 23, 2011
arielb1 pushed a commit to arielb1/rust that referenced this issue Apr 10, 2015
oli-obk pushed a commit to oli-obk/rust that referenced this issue Jul 19, 2017
…onstants

Detect modifications of immutable memory
keeperofdakeys pushed a commit to keeperofdakeys/rust that referenced this issue Dec 12, 2017
Fix undeclared type name errors when targeting android aarch64.
kazcw pushed a commit to kazcw/rust that referenced this issue Oct 23, 2018
* Add vroundps, vceilps, vfloorps, vsqrtps, vsqrtpd

* Uninhibit assert_instr on non-expanded intrinsics

Also use the new simd_test macro

* Use simd_test where possible

* Add automated tests for vround*

* Add target_feature guards to automated tests

* Move automated tests below their functions
rchaser53 pushed a commit to rchaser53/rust that referenced this issue Jan 19, 2019
jacob-hughes referenced this issue in jacob-hughes/alloy Apr 29, 2021
53: Tweaks to Boehm multithreaded API r=ltratt a=jacob-hughes

These are some minor changes that need fixing before this can be used properly in rustgc. Mostly because I misunderstood the way the Boehm API works the first time around.

Co-authored-by: Jake Hughes <jh@jakehughes.uk>
celinval pushed a commit to celinval/rust-dev that referenced this issue Nov 20, 2024
…t-lang#144)

# Description 
This PR introduces function contracts and proof harness for the NonNull
pointer in the Rust core library. Specifically, it verifies three new
APIs—`swap`, `replace`, and `drop_in_place` with Kani. These changes
enhance the functionality of memory operations for NonNull pointers.

# Change Overview
Covered APIs:
1. NonNull::swap: Swaps the values at two mutable locations of the same
type
2. NonNull::replace: Replaces the pointer's value, returning the old
value
3. NonNull::drop_in_place: Executes the destructor (if any) of the
pointed-to value

Resolves rust-lang#53 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
celinval pushed a commit to celinval/rust-dev that referenced this issue Nov 29, 2024
…_raw_parts`, `to_raw_parts` in NonNull (rust-lang#127)

Towards rust-lang#53 

Contracts and harnesses for `dangling`, `from_raw_parts`,
`slice_from_raw_parts`, `to_raw_parts` in NonNull
### Discussion

1. `NonNull::slice_from_raw_parts`:
[requested](model-checking/kani#3693) new Kani
API to compare byte by byte
2. `NonNull::to_raw_parts`: [unstable vtable comparison
'Eq'](model-checking#139)

### Verification Result
```
SUMMARY:
 ** 0 of 141 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.17378491s

Complete - 6 successfully verified harnesses, 0 failures, 6 total.
```

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
celinval pushed a commit to celinval/rust-dev that referenced this issue Dec 6, 2024
…_from` (rust-lang#103)

# Description:

This PR introduces function contracts and proof harness for the NonNull
pointer in the Rust core library. Specifically, it verifies three new
APIs—`byte_offset`, `byte_add`, and `byte_offset_from` with Kani. These
changes enhance the functionality of pointer arithmetic and verification
for NonNull pointers.

# Changes Overview:

**Covered APIs:**
1. `NonNull::byte_add`: Adds a specified byte offset to a pointer.
2. `NonNull::byte_offset`: Allows calculating an offset from a pointer
in bytes.
4. `NonNull::byte_offset_from`: Calculates the distance between two
pointers in bytes.

**Proof harness:**
1. `non_null_byte_add_proof`
2. `non_null_byte_offset_proof`
3. `non_null_byte_offset_from_proof`

Towards rust-lang#53
celinval pushed a commit to celinval/rust-dev that referenced this issue Dec 6, 2024
rust-lang#126)

### Description

This PR includes contracts and proof harnesses for the four APIs as_ptr,
cast, as_mut_ptr, and as_non_null_ptr which are part of the NonNull
library in Rust.

### Changes Overview:

Covered APIs:
NonNull::as_ptr: Acquires the underlying *mut pointer
NonNull::cast: Casts to a pointer of another type
NonNull:: as_mut_ptr:  Returns raw pointer to array's buffer
NonNull::as_non_null_ptr:  Returns a non-null pointer to slice's buffer

Proof harness:
non_null_check_as_ptr
non_null_check_cast
non_null_check_as_mut_ptr
non_null_check_as_non_null_ptr

Revalidation

To revalidate the verification results, run kani verify-std -Z
unstable-options "path/to/library" -Z function-contracts -Z
mem-predicates --harness ptr::non_null::verify. This will run all four
harnesses in the module. All default checks should pass:

```
SUMMARY:
 ** 0 of 128 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.8232234s

Complete - 4 successfully verified harnesses, 0 failures, 4 total.

```
Towards issue rust-lang#53  

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: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Co-authored-by: Zyad Hassan <zyadh@amazon.com>
Co-authored-by: Michael Tautschnig <mt@debian.org>
Co-authored-by: Qinyuan Wu <53478459+QinyuanWu@users.noreply.github.com>
carolynzech added a commit to celinval/rust-dev that referenced this issue Dec 13, 2024
…st-lang#107)

### **Description**
This PR includes contracts and proof harnesses for the four APIs,
`offset` ,` byte_sub`, `map_addr`, and `with_addr` which are part of the
NonNull library in Rust.

### **Changes Overview:**
Covered APIs:
NonNull::offset: Adds an offset to a pointer
NonNull::byte_sub: Calculates an offset from a pointer in bytes.
NonNull:: map_addr: Creates a new pointer by mapping self's address to a
new one
NonNull::with_addr: Creates a new pointer with the given address

Proof harness:
non_null_check_offset
non_null_check_byte_sub
non_null_check_map_addr
non_null_check_with_addr


### **Revalidation**

To revalidate the verification results, run kani verify-std -Z
unstable-options "path/to/library" -Z function-contracts -Z
mem-predicates --harness ptr::non_null::verify. This will run all four
harnesses in the module. All default checks should pass:

```

VERIFICATION:- SUCCESSFUL
Verification Time: 0.57787573s

Complete - 6 successfully verified harnesses, 0 failures, 6 total.
```
Towards issue rust-lang#53 

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: Carolyn Zech <cmzech@amazon.com>
Co-authored-by: Zyad Hassan <zyadh@amazon.com>
Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
carolynzech added a commit to celinval/rust-dev that referenced this issue Dec 13, 2024
…and copy_from_nonoverlapping (rust-lang#149)

Description

This PR includes contracts and proof harnesses for the four APIs
copy_to, copy_to_nonoverlapping, copy_from, and copy_from_nonoverlapping
which are part of the NonNull library in Rust.

Changes Overview:

Covered APIs:
NonNull::copy_to
NonNull::copy_to_nonoverlapping
NonNull::copy_from
NonNull::opy_from_nonoverlapping

Proof harness:
non_null_check_copy_to
non_null_check_copy_to_nonoverlapping
non_null_check_copy_from
non_null_check_copy_from_nonoverlapping,

Revalidation

To revalidate the verification results, run path_to/kani/scripts/kani
verify-std -Z unstable-options "path/to/library" -Z function-contracts
-Z mem-predicates --harness ptr::non_null::verify. This will run all
four harnesses in the module. All default checks should pass:

SUMMARY:
 ** 0 of 141 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.62114185s

Complete - 6 successfully verified harnesses, 0 failures, 6 total.

Towards issue rust-lang#53 

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: Qinyuan Wu <qinyuanw@andrew.cmu.edu>
Co-authored-by: Carolyn Zech <cmzech@amazon.com>
Co-authored-by: Qinyuan Wu <53478459+QinyuanWu@users.noreply.github.com>
Co-authored-by: Michael Tautschnig <mt@debian.org>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-frontend Area: Compiler frontend (errors, parsing and HIR)
Projects
None yet
Development

No branches or pull requests

2 participants