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

Native types should have crate-relative identifiers #149

Closed
pcwalton opened this issue Aug 13, 2010 · 1 comment
Closed

Native types should have crate-relative identifiers #149

pcwalton opened this issue Aug 13, 2010 · 1 comment

Comments

@pcwalton
Copy link
Contributor

Native type identifiers are global, not crate-relative. This doesn't seem easy to typecheck because of the diamond import problem:

Suppose:

  • Crate A defines a native type foo;
  • Crate B imports A and exports A.foo;
  • Crate C imports A and exports A.foo;
  • Crate D imports B and C and unifies B.foo and C.foo.

B.foo and C.foo won't be considered compatible.

Instead of having one global value set, we could subject them to crate-relative name resolution, just like any other type. In other words, we would have e.g. "TY_native of crate_id * native_id".

@graydon
Copy link
Contributor

graydon commented Jan 27, 2011

WONTFIX (not required for bootstrapping; code in rustc is all different. defs are all crate-relative there).

oli-obk pushed a commit to oli-obk/rust that referenced this issue Jul 19, 2017
…rder

fix argument order on check_align()
keeperofdakeys pushed a commit to keeperofdakeys/rust that referenced this issue Dec 12, 2017
Linkify more docs, add more tested triples
dlrobertson pushed a commit to dlrobertson/rust that referenced this issue Nov 29, 2018
Reorganise the special traits section
rchaser53 pushed a commit to rchaser53/rust that referenced this issue Jan 19, 2019
djtech-dev pushed a commit to djtech-dev/rust that referenced this issue Dec 9, 2021
antoyo added a commit to antoyo/rust that referenced this issue Jun 7, 2022
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 <[email protected]>
Co-authored-by: Carolyn Zech <[email protected]>
Co-authored-by: Qinyuan Wu <[email protected]>
Co-authored-by: Michael Tautschnig <[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
None yet
Projects
None yet
Development

No branches or pull requests

2 participants