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

Something is wrong with bind-obj-ctor.rs #59

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

Something is wrong with bind-obj-ctor.rs #59

graydon opened this issue Jun 23, 2010 · 1 comment
Labels
A-type-system Area: Type system

Comments

@graydon
Copy link
Contributor

graydon commented Jun 23, 2010

It seems we can't quite bind object constructors yet. This doesn't make much sense, since they are just functions.
@graydon
Copy link
Contributor Author

graydon commented Jan 27, 2011

Fixed, apparently, long ago. Works now.

@evanmcc evanmcc mentioned this issue Apr 3, 2012
Closed
oli-obk pushed a commit to oli-obk/rust that referenced this issue Jul 19, 2017
@solson
Merge pull request rust-lang#59 from oli-obk/master
1e3659e 
enable A<Struct> -> A<Trait> downcasting where `A<Trait>` is a fat pointer
kazcw pushed a commit to kazcw/rust that referenced this issue Oct 23, 2018
@alexcrichton
Uncomment _mm256_mpsadbw_epu8 (rust-lang#128)
afba6fc 
Just needed some `constify_imm8!` treatment

Closes rust-lang#59
bors pushed a commit to rust-lang-ci/rust that referenced this issue Oct 1, 2021
@workingjubilee
Merge pull request rust-lang#59 from rust-lang/blank-ish
4ad53da 
Add a blank issue template
djtech-dev pushed a commit to djtech-dev/rust that referenced this issue Dec 9, 2021
@TheDan64
Simplified EE creation by calling initialize native for the user.
7a06915 
Fixes rust-lang#59
@Amanieu Amanieu mentioned this issue Jun 12, 2023
Open
jaisnan pushed a commit to jaisnan/rust-dev that referenced this issue Oct 15, 2024
@Yenyun035 @rajathkotyal
Contracts & Harnesses for unchecked_add (rust-lang#91)
1bf01fd 
Towards rust-lang#59 

* Added contracts for `unchecked_add` (located in
`library/core/src/num/int_macros.rs` and `uint_macros.rs`)
* Added a harness for `unchecked_add` of each integer type
* `i8`, `i16`, `i32`, `i64`, `i128`, `isize`, `u8`, `u16`, `u32`, `u64`,
`u128`, `usize` --- 12 harnesses in total.

---------

Co-authored-by: yew005 <yew005@ucsd.edu>
Co-authored-by: Rajath Kotyal <53811196+rajathkotyal@users.noreply.github.com>
Co-authored-by: rajathmCMU <rajathkotyal@gmail.com>
jaisnan pushed a commit to jaisnan/rust-dev that referenced this issue Oct 15, 2024
@rajathkotyal @MWDZ
@lanfeima @Yenyun035
Contracts & Harnesses for unchecked_mul , unchecked_sub, `uncheck…
0de4670 
…ed_shl` and `unchecked_shr` (rust-lang#96)

Towards : issue rust-lang#59 

Parent branch :
[c-0011-core-nums-yenyunw-unsafe-ints](https://github.com/rajathkotyal/verify-rust-std/tree/c-0011-core-nums-yenyunw-unsafe-ints
) - Tracking PR rust-lang#91

---------

Co-authored-by: yew005 <yew005@ucsd.edu>
Co-authored-by: MWDZ <jinjunfeng721@gmail.com>
Co-authored-by: Lanfei Ma <99311320+lanfeima@users.noreply.github.com>
Co-authored-by: Yenyun035 <yenyunw@andrew.cmu.edu>
jaisnan pushed a commit to jaisnan/rust-dev that referenced this issue Oct 15, 2024
@Yenyun035 @rajathkotyal
Contracts and Harnesses for unchecked_neg (rust-lang#102)
32e0cf9 
Towards rust-lang#59 

### Changes
* Added contracts for `unchecked_neg` (located in
`library/core/src/num/int_macros.rs`)
* Added a harness for `unchecked_neg` of each signed integer type
  * `i8`, `i16`, `i32`, `i64`, `i128`, `isize` --- 6 harnesses in total.
* Fixed comments.

### Revalidation
1. Per the discussion in rust-lang#59, we have to **build and run Kani from
`feature/verify-rust-std` branch**.
2. To revalidate the verification results, run the following command.
`<harness_to_run>` can be either `num::verify` to run all harnesses or
`num::verify::<harness_name>` (e.g. `check_unchecked_neg_i8`) to run a
specific harness.
```
kani verify-std  "path/to/library" \
    --harness <harness_to_run> \
    -Z unstable-options \
    -Z function-contracts \
    -Z mem-predicates
```

All default harnesses should pass.

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: yew005 <yew005@ucsd.edu>
Co-authored-by: Rajath Kotyal <53811196+rajathkotyal@users.noreply.github.com>
Co-authored-by: rajathmCMU <rajathkotyal@gmail.com>
jaisnan pushed a commit to jaisnan/rust-dev that referenced this issue Oct 15, 2024
@rajathkotyal
Contracts & Harnesses for widening_mul (rust-lang#111)
dc862c4 
Towards : issue rust-lang#59

Parent branch : main 

Revalidation : 
Per the discussion in
model-checking#59, we have to
build and run Kani from feature/verify-rust-std branch.
To revalidate the verification results, run the following command.
<harness_to_run> can be either num::verify to run all harnesses or
num::verify::<harness_name> (e.g. widening_mul_u16_small) to run a
specific harness.
```
kani verify-std  "path/to/library" \
    --harness <harness_to_run> \
    -Z unstable-options \
    -Z function-contracts \
    -Z mem-predicates
```
jaisnan pushed a commit to jaisnan/rust-dev that referenced this issue Oct 22, 2024
@Yenyun035
Contracts & Harnesses for wrapping_shl (rust-lang#112)
3a967e3 
Towards rust-lang#59 

### Changes
* Added contracts for `wrapping_shl` (located in
`library/core/src/num/int_macros.rs` and `uint_macros.rs`)
* Added a macro for generating wrapping_{shl, shr} harnesses
* Added harnesses for `wrapping_shl` of each integer type
* `i8`, `i16`, `i32`, `i64`, `i128`, `isize`, `u8`, `u16`, `u32`, `u64`,
`u128`, `usize` --- 12 harnesses in total.

### Revalidation
1. Per the discussion in rust-lang#59, we have to **build and run Kani from
`feature/verify-rust-std` branch**.
2. To revalidate the verification results, run the following command.
`<harness_to_run>` can be either `num::verify` to run all harnesses or
`num::verify::<harness_name>` (e.g. `checked_wrapping_shl_i8`) to run a
specific harness.
```
kani verify-std  "path/to/library" \
    --harness <harness_to_run> \
    -Z unstable-options \
    -Z function-contracts \
    -Z mem-predicates
```

All harnesses should pass the default checks (1251 checks where 1
unreachable).
```
SUMMARY:
 ** 0 of 1251 failed (1 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 2.4682913s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.
```
Example of the unreachable check:
```
Check 123: num::<impl i8>::wrapping_shl.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to subtract with overflow"
         - Location: library/core/src/num/int_macros.rs:2172:42 in function num::<impl i8>::wrapping_shl
```

### Questions
1. Should we add `requires` (and `ensures`) for `wrapping_shl` given
that `unchecked_shl` already has a `requires`?

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
jaisnan pushed a commit to jaisnan/rust-dev that referenced this issue Oct 29, 2024
@lanfeima @MWDZ
@Yenyun035 @rajathkotyal
Harnesses for carrying_mul (rust-lang#114)
c4a1f45 
## Towards: Issue rust-lang#59

### Parent branch: main

---

### Changes


- Added macros for generating `carrying_mul` harnesses
- Added harnesses for `carrying_mul` for the following integer types:
  - `u8`, `u16`, `u32`, `u64`

---------

Co-authored-by: yew005 <yew005@ucsd.edu>
Co-authored-by: MWDZ <jinjunfeng721@gmail.com>
Co-authored-by: Yenyun035 <yenyunw@andrew.cmu.edu>
Co-authored-by: Rajath <rajathkotyal@gmail.com>
Co-authored-by: Rajath Kotyal <53811196+rajathkotyal@users.noreply.github.com>
celinval pushed a commit to celinval/rust-dev that referenced this issue Dec 6, 2024
@Yenyun035 @rajathkotyal
@MWDZ @zhassan-aws
Contracts & Harnesses for f{32,64}::to_int_unchecked (rust-lang#134)
72323e4 
Towards / Resolves rust-lang#59 

(Resolved) Depends on [this Kani
Issue](model-checking/kani#3629) and [this
PR](model-checking/kani#3660), as discussed in
[this
thread](model-checking#59 (comment))
in rust-lang#59

(Resolved) Depends on [this Kani
Issue](model-checking/kani#3711) and [this
PR](model-checking/kani#3742)

(Resolved) Waiting for Kani PR#3742 merged into
`feature/verify-rust-std`

f16 and f128 are in rust-lang#163 

### Changes
* Added contracts for `f{32,64}::to_int_unchecked` (located in
`library/core/src/num/f{32,64}.rs`)
* Added a macro for generating `to_int_unchecked` harnesses
* Added harnesses for `f{32,64}to_int_unchecked` of each integer type
* `i8`, `i16`, `i32`, `i64`, `i128`, `isize`, `u8`, `u16`, `u32`, `u64`,
`u128`, `usize` --- 12 harnesses in total.

### Verification Results
To compile, we need to add the `-Z float-lib` flag.
```
Checking harness num::verify::checked_f32_to_int_unchecked_usize...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 6.424911s

Checking harness num::verify::checked_f64_to_int_unchecked_u128...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 6.8557353s

Checking harness num::verify::checked_f32_to_int_unchecked_u16...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 6.195041s

Checking harness num::verify::checked_f32_to_int_unchecked_i8...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 6.2361426s

Checking harness num::verify::checked_f64_to_int_unchecked_i32...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 6.3952055s

Checking harness num::verify::checked_f64_to_int_unchecked_i128...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 7.5295496s

Checking harness num::verify::checked_f64_to_int_unchecked_u16...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 6.2897367s

Checking harness num::verify::checked_f32_to_int_unchecked_i64...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 6.58576s

Checking harness num::verify::checked_f64_to_int_unchecked_i16...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 6.2046432s

Checking harness num::verify::checked_f32_to_int_unchecked_i128...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 6.8473463s

Checking harness num::verify::checked_f32_to_int_unchecked_u8...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 6.131122s

Checking harness num::verify::checked_f32_to_int_unchecked_i16...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 6.436728s

Checking harness num::verify::checked_f32_to_int_unchecked_u128...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 6.666422s

Checking harness num::verify::checked_f64_to_int_unchecked_u8...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 6.17829s

Checking harness num::verify::checked_f32_to_int_unchecked_i32...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 6.6507607s

Checking harness num::verify::checked_f64_to_int_unchecked_i64...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 7.3081775s

Checking harness num::verify::checked_f64_to_int_unchecked_u64...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 7.0912967s

Checking harness num::verify::checked_f64_to_int_unchecked_i8...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 6.4602604s

Checking harness num::verify::checked_f64_to_int_unchecked_usize...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 6.9098988s

Checking harness num::verify::checked_f64_to_int_unchecked_u32...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 6.557031s

Checking harness num::verify::checked_f64_to_int_unchecked_isize...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 7.1193557s

Checking harness num::verify::checked_f32_to_int_unchecked_u64...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 6.7919626s

Checking harness num::verify::checked_f32_to_int_unchecked_u32...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 6.557074s

Checking harness num::verify::checked_f32_to_int_unchecked_isize...

VERIFICATION RESULT:
 ** 0 of 136 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 6.710118s

Complete - 24 successfully verified harnesses, 0 failures, 24 total.
```
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: rajathmCMU <rajathkotyal@gmail.com>
Co-authored-by: MWDZ <jinjunfeng721@gmail.com>
Co-authored-by: Zyad Hassan <zyadh@amazon.com>
carolynzech pushed a commit to ReinierMaas/rust that referenced this issue Dec 6, 2024
@Yenyun035
Close Challenge 11 (rust-lang#206)
e70a892 
Resolves rust-lang#59

### Changes
* Marked Challenge 11 as resolved
* Changed the end date of the challenge
* Added the contributors
This issue was closed.
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
1 participant
@graydon