List view

Tracking issue for function and method stubbing

T-RFCLabel RFC PRs and IssuesLabel RFC PRs and Issues

Z-Kani CompilerIssues that require some changes to the compilerIssues that require some changes to the compiler

Status: Open.

#1809 In model-checking/kani;

· aaronbembenek-aws opened on Oct 27, 2022

Split tests for function/method stubbing into multiple harnesses

[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.

[I] Refactoring / Clean UpRefactoring or cleaning up of existing codeRefactoring or cleaning up of existing code

Status: Open.

#1861 In model-checking/kani;

· aaronbembenek-aws opened on Nov 7, 2022

Allow generic parameter names to differ while validating function/method stubs

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.

Status: Open.

#1953 In model-checking/kani;

· aaronbembenek-aws opened on Nov 30, 2022

Resolve trait methods for stubs and function contracts

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.

T-UserTag user issues / requestsTag user issues / requests

Z-ContractsIssue related to code contractsIssue related to code contracts

Status: Open.

#1997 In model-checking/kani;

· aaronbembenek-aws opened on Dec 13, 2022

Address validation of stubs with mismatched lifetimes

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.

Status: Open.

#2007 In model-checking/kani;

· aaronbembenek-aws opened on Dec 15, 2022

Implement stub-sets

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

Status: Open.

#2096 In model-checking/kani;

· celinval opened on Jan 9, 2023

Print all the stubs that were exercised in a harness

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

Status: Open.

#2119 In model-checking/kani;

· celinval opened on Jan 13, 2023

Avoid unnecessary allocations in MIR passes

[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.

Z-Kani CompilerIssues that require some changes to the compilerIssues that require some changes to the compiler

Status: Open.

#2664 In model-checking/kani;

· feliperodri opened on Aug 8, 2023

Stub of foreign function fail name resolution

[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.

Status: Open.

#2686 In model-checking/kani;

· celinval opened on Aug 15, 2023

FFI stubbing for libc crate only works if libc crate is imported via <code>feature(rustc_private)</code>

[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.

Status: Open.

#2673 In model-checking/kani;

· roypat opened on Aug 11, 2023