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

Extend name resolution to support qualified paths (Partial Fix) #3457

Merged
merged 6 commits into from
Aug 30, 2024

Conversation

celinval
Copy link
Contributor

@celinval celinval commented Aug 22, 2024

This is the first part needed for us to add support to stubbing trait implementations (#1997) and primitive types (#2646).

After this change, we need to change stubs to accept a FnResolution instead of FnDef. We also need to find out how to retrieve methods of primitive types.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@celinval celinval requested a review from a team as a code owner August 22, 2024 01:55
@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Aug 22, 2024
This is the first part needed for us to add support to stubbing
trait implementations and primitive types.

After this change, we need to change stubs to accept a `FnResolution`
instead of `FnDef`. We also need to find out how to retrieve methods
of primitive types.
Copy link
Contributor

@zhassan-aws zhassan-aws left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

kani-compiler/src/kani_middle/attributes.rs Outdated Show resolved Hide resolved
kani-compiler/src/kani_middle/attributes.rs Outdated Show resolved Hide resolved
Co-authored-by: Felipe R. Monteiro <[email protected]>
@celinval celinval changed the title Extend name resolution to support qualified paths Extend name resolution to support qualified paths (Partial Fix) Aug 30, 2024
@celinval celinval added this pull request to the merge queue Aug 30, 2024
Merged via the queue into model-checking:main with commit 01a00b0 Aug 30, 2024
27 checks passed
github-merge-queue bot pushed a commit that referenced this pull request Sep 4, 2024
These are the auto-generated release notes:

## What's Changed
* Update CBMC build instructions for Amazon Linux 2 by @tautschnig in
#3431
* Handle intrinsics systematically by @artemagvanian in
#3422
* Bump tests/perf/s2n-quic from `445f73b` to `ab9723a` by @dependabot in
#3434
* Automatic cargo update to 2024-08-12 by @github-actions in
#3433
* Actually apply CBMC patch by @tautschnig in
#3436
* Update features/verify-rust-std branch by @feliperodri in
#3435
* Add test related to issue 3432 by @celinval in
#3439
* Implement memory initialization state copy functionality by
@artemagvanian in #3350
* Bump tests/perf/s2n-quic from `ab9723a` to `80b93a7` by @dependabot in
#3453
* Make points-to analysis handle all intrinsics explicitly by
@artemagvanian in #3452
* Automatic cargo update to 2024-08-19 by @github-actions in
#3450
* Add loop scanner to tool-scanner by @qinheping in
#3443
* Avoid corner-cases by grouping instrumentation into basic blocks and
using backward iteration by @artemagvanian in
#3438
* Re-enabled hierarchical logs in the compiler by @celinval in
#3449
* Fix ICE due to mishandling of Aggregate rvalue for raw pointers to
`str` by @celinval in #3448
* Automatic cargo update to 2024-08-26 by @github-actions in
#3459
* Bump tests/perf/s2n-quic from `80b93a7` to `8f7c04b` by @dependabot in
#3460
* Update deny action by @zhassan-aws in
#3461
* Basic support for memory initialization checks for unions by
@artemagvanian in #3444
* Adjust test patterns so as not to check for trivial properties by
@tautschnig in #3464
* Clarify comment in RFC Template by @carolynzech in
#3462
* RFC: Source-based code coverage by @adpaco-aws in
#3143
* Adopt Rust's source-based code coverage instrumentation by @adpaco-aws
in #3119
* Upgrade toolchain to 08/28 by @jaisnan in
#3454
* Extra tests and bug fixes to the delayed UB instrumentation by
@artemagvanian in #3419
* Upgrade Toolchain to 8/29 by @carolynzech in
#3468
* Automatic toolchain upgrade to nightly-2024-08-30 by @github-actions
in #3469
* Extend name resolution to support qualified paths (Partial Fix) by
@celinval in #3457
* Partially integrate uninit memory checks into `verify_std` by
@artemagvanian in #3470
* Update Toolchain to 9/1 by @carolynzech in
#3478
* Automatic cargo update to 2024-09-02 by @github-actions in
#3480
* Bump tests/perf/s2n-quic from `8f7c04b` to `1ff3a9c` by @dependabot in
#3481
* Automatic toolchain upgrade to nightly-2024-09-02 by @github-actions
in #3479
* Automatic toolchain upgrade to nightly-2024-09-03 by @github-actions
in #3482
* RFC for List Subcommand by @carolynzech in
#3463
* Add tests for fixed issues. by @carolynzech in
#3484


**Full Changelog**:
kani-0.54.0...kani-0.55.0

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-BenchCI Tag a PR to run benchmark CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants