Autoharness: support slice and string arguments (bounded) by tautschnig · Pull Request #4691 · model-checking/kani

tautschnig · 2026-07-29T01:38:08Z

Description

Autoharness can now generate harnesses for functions with &[T]/&mut [T] arguments (where T implements or can derive Arbitrary) and &str arguments — strictly opt-in via a new --bounded-arguments option, since such inputs are necessarily bounded and a verification result then only holds up to the bound. In the top-100 crates.io evaluation, these argument types accounted for ~1,400 skipped functions.

Opt-in and reporting design (bounded results must never masquerade as unbounded ones):

Without --bounded-arguments (the default), behavior only changes in that eligible functions are skipped with a new, actionable reason: Requires --bounded-arguments for argument(s) ....
With it, such harnesses are marked (bounded) in the "Kind of Automatic Harness" column (via a new HarnessMetadata::is_bounded field), and a note after the summary table spells out the caveat.

Generation: AnySliceRef returns &mut storage[..len] with nondet len (reborrowed as shared for &[T]), bounded at 16 elements, backed by a harness-local nondet array; AnyStrRef returns the longest valid-UTF-8 prefix of nondet bytes, bounded at 4 — full UTF-8 coverage including multi-byte characters (cover-checked), reusing the algorithm of String's BoundedArbitrary impl. Measured: assuming from_utf8(..).is_ok() is intractable even at bound 4, while the prefix formulation costs ~10s@4 / 28s@8 / 180s@16; the string bound was therefore lowered to 4 so that a char-decoding harness (e.g. s.chars()...) stays within the default 60s harness timeout (on slow CI runners even 4 can approach it, so the test raises --harness-timeout). Both bounds sit below the default unwind bound of 20.

Also eliminates the argument-position vs. field-position cache-poisoning hazard class outright: top-level argument verdicts are no longer inserted into the shared Arbitrary cache (implements_arbitrary memoizes its own recursion).

Follow-up work is planned to explore unbounded generation for these types (e.g. via loop contracts or CBMC's unbounded-array reasoning), at which point the flag could be retired for them.

Testing

New script-based test cargo_autoharness_slices exercising both modes: without the flag it asserts the Requires --bounded-arguments skip reason; with the flag it checks per-function results (safe consumption passes; OOB indexing on possibly-empty slices/strings fails, correctly), the (bounded) markers, the post-table note, and four cover checks proving non-vacuity (empty slice, max-length slice with specific contents, 3-byte string with specific prefix, string starting with a non-ASCII character — all SATISFIED).

Updated cargo_autoharness_filter. Full autoharness + autoderive suites, verify_std_cmd/std_codegen, and kani-compiler/kani-driver/kani_metadata unit tests pass.

Towards #3832

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

Copilot

Pull request overview

This PR extends Kani’s autoharness generation to support slice reference arguments (&[T], &mut [T]) and string slice arguments (&str) by generating bounded, harness-owned backing storage and returning a nondeterministic-length prefix (bounded at 16). It also documents the resulting soundness/coverage caveats (bounded length; ASCII-only strings) and adds a script-based regression test suite to exercise the new behavior.

Changes:

Add AnySliceRefModel / AnyStrRefModel models in kani_core to produce bounded-length slice/&str references from harness-owned storage.
Update the compiler’s automatic harness generation to recognize slice/&str arguments, allocate backing locals, and call the new models.
Add a new script-based test (cargo_autoharness_slices) and update the autoharness filter expected output to reflect slice-arg support.

Reviewed changes

Copilot reviewed 13 out of 13 changed files in this pull request and generated no comments.

Show a summary per file

File	Description
tests/script-based-pre/cargo_autoharness_slices/src/lib.rs	New test crate with functions covering `&[T]`, `&mut [T]`, and `&str` argument handling (pass/fail/skip + cover checks).
tests/script-based-pre/cargo_autoharness_slices/slices.sh	Script invoking `cargo kani autoharness -Z autoharness` for the new test.
tests/script-based-pre/cargo_autoharness_slices/slices.expected	Expected summary output including cover satisfiability and per-function results.
tests/script-based-pre/cargo_autoharness_slices/config.yml	Script-based test configuration (expects nonzero exit due to intentional failures).
tests/script-based-pre/cargo_autoharness_slices/Cargo.toml	Test crate manifest (edition 2024 + kani cfg lint config).
tests/script-based-pre/cargo_autoharness_filter/src/lib.rs	Adjust filter test to include a slice-arg function as supported.
tests/script-based-pre/cargo_autoharness_filter/filter.expected	Update expected counts/output to account for the newly supported slice-arg function.
library/kani_core/src/arbitrary.rs	Add `any_slice_ref` and `any_str_ref` model functions used by compiler-generated harnesses.
kani-compiler/src/kani_middle/transform/automatic.rs	Teach `call_kani_any_for_ty` to synthesize bounded slice/`&str` arguments via backing locals + model calls; add bound constant and new model FnDefs.
kani-compiler/src/kani_middle/mod.rs	Add `autoharness_supported_arg_ty` helper that treats slice refs and `&str` as supported argument-position types.
kani-compiler/src/kani_middle/kani_functions.rs	Register new `KaniModel` variants for the slice/str reference models.
kani-compiler/src/kani_middle/codegen_units.rs	Use `autoharness_supported_arg_ty` for arg eligibility; avoid caching slice/str-ref verdicts to prevent cache poisoning.
docs/src/reference/experimental/autoharness.md	Document slice/`&str` support, including the bound and ASCII-only caveats.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

### Description `Box<T>` implements `Arbitrary`, but `Rc<T>` and `Arc<T>` did not, so functions taking reference-counted arguments could not be verified against nondeterministic inputs — and were skipped by `kani autoharness` with "Missing Arbitrary implementation" (smart-pointer receivers are among the largest skip classes in the top-100 crates.io evaluation). This PR adds the analogous implementations. Note that unlike slice/container arguments (model-checking#4691/model-checking#4693), these need no bound and no opt-in flag: a smart pointer to `T` covers exactly the values of `T`, so the generated values retain Kani's usual full-coverage guarantee. A follow-up will extend autoharness to smart pointers around types that only *can-derive* `Arbitrary` (compiler-synthesized implementations); that requires compiler-side models that depend on `alloc` and hence some optional-model plumbing for the `no_core` flow. ### Testing New test `tests/kani/Arbitrary/rc_arc.rs` with cover checks proving extreme values, specific values, and nested smart pointers (`Rc<Arc<u8>>`) are all generated (all SATISFIED). The `Arbitrary` suite and `kani` library unit/doc tests pass; verified via autoharness that `Rc<T>`/`Arc<T>`-taking functions are now selected and verified. Towards model-checking#3832 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: Kiro <kiro-agent@users.noreply.github.com>

Functions taking &[T]/&mut [T] (with T implementing or capable of deriving Arbitrary) or &str were previously skipped with 'Missing Arbitrary implementation'; in an evaluation across the top-100 crates.io crates these argument types alone accounted for ~1400 skipped functions. With the new --bounded-arguments option, the generated harness produces a slice of nondeterministic length, backed by a nondeterministic array stored in a dedicated harness local, via two new models: AnySliceRef returns '&mut storage[..len]' with nondeterministic len (reborrowed as shared for &[T] arguments), bounded at 16 elements; AnyStrRef returns the longest valid-UTF-8 prefix of the nondeterministic bytes, bounded at 8 bytes, reusing the algorithm of String's BoundedArbitrary implementation (computing the valid prefix is a deterministic function of the bytes, which symbolic execution handles well, whereas assuming from_utf8().is_ok() is intractable even at a bound of 4 bytes; measured cost 10s@4/28s@8/180s@16, so bound 8 stays within the default 60s harness timeout). Because a verification result for such a harness only holds up to the bound -- a bug that requires a larger input will not be found -- bounded harness generation is strictly opt-in and visibly reported: - without --bounded-arguments, eligible functions are skipped with the new reason 'Requires --bounded-arguments for argument(s) ...'; - with the option, such harnesses are marked '(bounded)' in the summary table (via a new HarnessMetadata::is_bounded field), and a note after the table spells out the caveat. Both bounds sit below Kani's default unwinding bound of 20 so that loops over generated slices can be fully unwound by default. Like raw pointers (model-checking#4678), slice references are supported in argument position only, where the harness owns the backing storage. Top-level argument verdicts are no longer inserted into the shared Arbitrary cache at all, eliminating the argument-position vs. field-position cache-poisoning hazard class (implements_arbitrary memoizes its own recursion, so repeated argument types stay cheap). Towards model-checking#3832 Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

kani::any::<[T; N]>() is unresolvable when T's Arbitrary implementation is compiler-derived ([T; N]'s blanket impl requires T: Arbitrary), so slice arguments with such element types crashed harness generation. Found by re-running the top-100 crates.io evaluation (e.g. aho-corasick's &[StateID] arguments); regression-tested with a derivable-element slice argument. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

The cargo_autoharness_slices regression test timed out (CBMC hit the 60s autoharness harness timeout) on the count_a harness across all CI runners. count_a fully decodes every char (s.chars().filter(...).count()), which unwinds the decoding loop to the default bound (20) over symbolic bytes; at 8 nondeterministic bytes this blows up to ~3.1M clauses and exceeds 60s. Lower AUTOHARNESS_STR_BOUND from 8 to 4. This keeps all str_cover cover checks satisfiable (they need at most 3 bytes) and brings the char-decoding harness well within the timeout, while slices are unaffected (bound 16).

Copilot

Pull request overview

Copilot reviewed 21 out of 21 changed files in this pull request and generated 5 comments.

- Raise the harness timeout for the cargo_autoharness_slices test so the char-decoding count_a harness does not spuriously time out on slow CI runners (macos-15-intel). - Validate the cargo kani --list status in slices.sh instead of masking it behind the grep pipeline. - Assert each of the four cover descriptions together with its SATISFIED status, so regressions in boundary/UTF-8 generation are detected. - Serialize is_bounded in create_harness_metadata_json (--export-json) and cover the true case in the unit test. - Reconcile the autoharness docs so the bounded-arguments exception is not contradicted by the 'without bounds' eligibility statement. - Clarify the AUTOHARNESS_STR_BOUND comment about slow-machine timeouts.

Copilot

Pull request overview

Copilot reviewed 22 out of 22 changed files in this pull request and generated 1 comment.

The per-harness progress line printed "against all possible inputs" for every automatically generated harness, including bounded ones, which contradicts the reporting guarantee that bounded results must not masquerade as exhaustive. Branch on is_bounded so bounded harnesses print "against all possible inputs (bounded for some arguments)", and assert the qualified message in the cargo_autoharness_slices test.

Copilot

Pull request overview

Copilot reviewed 23 out of 23 changed files in this pull request and generated 1 comment.

…iasing Each reference/pointer/slice/string argument is generated from independent storage, so autoharness does not explore aliasing between distinct arguments (e.g. two &T arguments never share an address). This is a pre-existing underapproximation of all reference arguments -- not specific to --bounded-arguments -- so document it in the Limitations section rather than changing generation semantics.

…rgument aliasing

…4693) ### Description **Stacked on model-checking#4691** (only the last commit is new; review that one). Autoharness can now generate harnesses for arguments whose types implement `BoundedArbitrary` rather than `Arbitrary` — reusing Kani's existing machinery (the trait, its `Vec<T>`/`String`/`Box<[T]>` implementations, and `#[derive(BoundedArbitrary)]`) directly: the generated harness calls `kani::bounded_any::<T, 4>()`. Detection uses the same `Instance`-resolution approach as `implements_arbitrary`, enabled by a new `fn_marker` on `kani::bounded_any`. Like the slice/string support in model-checking#4691, this is **gated behind `--bounded-arguments`** and reported: without the flag, eligible functions are skipped with `Requires --bounded-arguments for argument(s) ...`; with it, harnesses are marked `(bounded)` in the summary table and the post-table note spells out that results only hold up to the bound. The bound of 4 is measured, not guessed: `BoundedArbitrary` values are heap allocated, and `String`'s implementation reasons about UTF-8 validity — at bound 8, even a trivial `String`-consuming harness exceeds the default 60s harness timeout. Follow-up work is planned to explore unbounded generation for container types. ### Testing New script-based test `cargo_autoharness_bounded` exercising both modes: the skip-reason hint without the flag; with the flag, `Vec<u8>`/`String` consumption (passes), OOB indexing on possibly-empty values (fails, correctly), a user struct deriving `BoundedArbitrary` with a `#[bounded]` field (passes), a cover check proving max-length vectors with specific contents are generated (SATISFIED), and graceful skipping of `Vec<Vec<u8>>`. Full autoharness suite, `verify_std_cmd`/`std_codegen`, and compiler/driver/metadata unit tests pass. Towards model-checking#3832 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: Kiro <kiro-agent@users.noreply.github.com> Co-authored-by: Felipe Monteiro <felisous@amazon.com>

…ields (model-checking#4694) ### Description `can_derive_arbitrary` recursed into reference *field* types, so a struct with a `&'static` reference field (reference fields with lifetime parameters were already rejected via the ADT's generic arguments) was deemed derivable. The compiler-synthesized `any()` then created the referent's storage inside its own body and returned a dangling reference, so the generated harness failed spuriously with "dereference failure: dead object" — a false alarm the user can do nothing about. Reject reference fields in the derivability check; such functions are now skipped with the usual "Missing Arbitrary implementation" reason. Top-level reference *arguments* are unaffected: for those the generated harness itself owns the referent's storage, which outlives the call. Found while implementing model-checking#4691 (the storage-lifetime asymmetry between argument position and field position is exactly what that PR documents for slices). ### Testing New script-based test `cargo_autoharness_ref_field`: asserts the struct-with-reference-field function is skipped (previously: spurious dead-object failure) while a plain `&u32` argument remains supported. Formatting and the compiler unit tests 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: Kiro <kiro-agent@users.noreply.github.com> Co-authored-by: Felipe Monteiro <felisous@amazon.com>

…odel-checking#4698) ### Description **Stacked on model-checking#4697** (only the last commit is new; review that one). `Box<T>`/`Rc<T>`/`Arc<T>` arguments were only supported by autoharness when `T` itself implements `Arbitrary` (resolving the blanket impls). When `T` merely *can derive* `Arbitrary` — the common case for plain structs without kani annotations — such arguments were skipped. This PR adds three generation models (`any_box`/`any_rc`/`any_arc`) whose internal `kani::any::<T>()` call gets the compiler-synthesized `Arbitrary` implementation via `AutomaticArbitraryPass`, exactly as for direct arguments of such types. Two design points: - **Optional models.** The models require `alloc`, so they exist only in the `kani` library, not `core::kani`. This introduces `KaniModel::is_optional()`: `validate_kani_functions` tolerates their absence and the autoharness passes hold them as `Option<FnDef>`, gracefully rejecting smart-pointer arguments in flows where they're unavailable (`kani verify-std` re-validated with `--force-rerun` to make sure the run wasn't cached). - **Robust detection.** `Box` via `is_box()`, `Rc`/`Arc` via their rustc diagnostic items (no name matching), plus a return-type equality check on the resolved model instance — which also correctly rejects non-default allocators (`Box<T, A>`); an arity-based check would have wrongly rejected plain `Box<T>` (= `Box<T, Global>`). Per the bounded-features policy (model-checking#4691/model-checking#4693): these values are **unbounded** — a smart pointer to `T` covers exactly the values of `T` — so they need no `--bounded-arguments` gating and retain the full-coverage guarantee, demonstrated by a cover check in the test. ### Testing New script-based test `cargo_autoharness_smart_pointers`: `Box`/`Rc`/`Arc` of both implementing and only-derivable pointees (all verified), a full-coverage cover check on the pointee (SATISFIED) with a correctly failing assertion, and graceful skipping of a pointee that can neither implement nor derive `Arbitrary`. Full autoharness suite (14 tests), `verify_std_cmd`/`std_codegen` (force-rerun), and `kani-compiler` unit tests pass. Towards model-checking#3832 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: Kiro <kiro-agent@users.noreply.github.com> Co-authored-by: Felipe Monteiro <felisous@amazon.com>

…odel-checking#4717) ### Description The top-100/500 crates.io failure triage (model-checking#3832) showed the largest class of genuine false alarms is nondeterministic receivers violating private type invariants: e.g. time's `Date` packs a validated ordinal into a private field, so raw field synthesis produces invalid dates and fails every method harness (194+ harnesses in the top-100 triage attributed to this class). Under the new opt-in `--constructor-args` flag, `kani::any::<T>` for private-field structs is synthesized as: generate nondeterministic constructor arguments, call one of `T`'s public constructors, assume success (switching on the discriminant for `Option<Self>`/`Result<Self, E>` returns), and return the payload. Constructor search prefers `Self` over `Option<Self>` over `Result<Self, E>` returns, then more arguments over fewer; it excludes non-public, doc-hidden (`_unchecked` macro exports that assert preconditions), unsafe, zero-argument (`Instant::now()` reaches unsupported `clock_gettime`; single-point coverage regardless), and generic constructors — each exclusion was validated empirically on the time crate. Per the bounded-features policy (model-checking#4691 discussion), the option is opt-in because it under-approximates (only constructor-reachable values are explored): harnesses are marked "(ctor)" via new `is_ctor_based` metadata, with an explanatory note in the summary. The sound successor (mining the type's own validity assertions into filters) is a follow-up PR building on this one. Measured on time-0.3.54: 341 -> 538 verified, 500 -> 315 failures (203 false alarms eliminated; 17 new failures from constructors with documented panics, a logged refinement). Note that constructor arguments must themselves already implement `Arbitrary` (they do not get the argument-position extensions — slices, smart pointers, nested constructors). Besides keeping phase 1 small, that requirement is what makes recursive and mutually-recursive constructors (`fn combine(a: Node, b: u32) -> Node`, or `A::from_b`/`B::from_a`) structurally unreachable, so generation cannot recurse forever. Verified by hand. #### Changes from the original branch (rebase onto main) `main` gained `--bounded-arguments`, per-parameter generic instantiation and the JSON frontend since this branch was cut, which surfaced three defects: - **`--bounded-arguments` was silently ignored.** The branch replaced the `bounded_arguments` parameter of `add_auto_harness_args` with `constructor_args` instead of adding to it. Both are now forwarded and *compose*: a harness that is both reads `#[kani::proof] (bounded) (ctor)` and both explanatory notes print independently. The compiler side carries an `AutoHarnessCaveats { is_bounded, is_ctor_based }` struct rather than reusing `main`'s single `bool` slot, so the two independent flags cannot be swapped at a call site. - **The "(ctor)" marker could lie.** `uses_ctor_generation` also accepted `find_unchecked_constructor`, but nothing in `AutomaticArbitraryPass` used that search — and `automatic::inline_with_assumed_panics`, the consumer named in its doc comment, does not exist. A type whose only constructor was an `_unchecked` builder was therefore marked "(ctor)" and given the under-approximation caveat while generation actually fell back to raw field synthesis. Reproduced, then fixed by making the marking predicate test exactly what generation tests; `find_unchecked_constructor` (75 lines, no remaining callers) was removed rather than shipped as dead code, and the follow-up should reintroduce it with its consumer. Pinned by a new `OnlyUnchecked` case in the test. - **`is_ctor_based` was missing from the JSON export.** `frontend/schema_utils.rs` emitted `is_bounded` only, so a JSON consumer could tell a bounded run apart but not a constructor-based one. Added and asserted in `schema_utils_test.rs`. Also adapted to `VariantDef::idx` no longer being public (reconstructed via `VariantIdx::to_val`, as `generate_enum_body` already does) and routed the pass through `main`'s shared `AnyModels` instead of duplicating `kani_any`/`kani_assume` fields. ### Testing `cargo_autoharness_constructor` runs the same crate with and without the flag: without, the invariant-violating false alarms appear; with it, they disappear and the affected harnesses carry the "(ctor)" marker. It covers a `Option<Self>`-returning constructor (`Day`), a direct-returning one (`Celsius`), a `Result<Self, E>`-returning one (`Even`), and a type with only an `_unchecked` constructor (`OnlyUnchecked`) that must *not* be marked. All 23 script-based autoharness tests pass, as does the full `script-based-pre` suite, `cargo test -p kani-driver`/`-p kani-compiler`/`-p kani_metadata`, `clippy --workspace --tests`, and `kani-fmt --check`. Towards model-checking#3832. 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: Kiro <kiro-agent@users.noreply.github.com> Co-authored-by: Felipe R. Monteiro <felisous@amazon.com>

model-checking#680) The analyzer keeps its own copy of `AutoHarnessSkipReason` and fails to deserialize metadata from current Kani, which changed `GenericFn` to `GenericFn(String)` (model-checking/kani#4679) and added `RequiresBoundedArguments` (model-checking/kani#4691). - Bring the enum in line with `kani_metadata`, keeping the `strum` strings identical so table text matches `kani autoharness --list`. - Normalize a bare `"GenericFn"` to `{"GenericFn": ""}` before `from_value`, since CI builds the pinned Kani, which still writes the old form. - Report `RequiresBoundedArguments` in its own type-category table instead of folding it into the missing-implementation one; the two need different remediation. - Note `--bounded-arguments` in the README. Verified with three hand-built `kani-metadata.json` fixtures (old format, `GenericFn` with payload, `RequiresBoundedArguments`): before the change they behave as described in model-checking#679, after it all three pass. `cargo test` covers the same three cases inline. Not run against a full std sweep. Resolves model-checking#679 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: Srivatsan Samraj <321934658+srivatsansamraj@users.noreply.github.com>

tautschnig requested a review from a team as a code owner July 29, 2026 01:38

Copilot AI review requested due to automatic review settings July 29, 2026 01:38

github-actions Bot added Z-EndToEndBenchCI Tag a PR to run benchmark CI Z-CompilerBenchCI Tag a PR to run benchmark CI labels Jul 29, 2026

Copilot started reviewing on behalf of tautschnig July 29, 2026 01:38

View session

Copilot AI reviewed Jul 29, 2026

View reviewed changes

tautschnig force-pushed the autoharness-bounded-slices branch from 4f2fc96 to f9cee0d Compare July 29, 2026 08:13

tautschnig mentioned this pull request Jul 29, 2026

Autoharness: support BoundedArbitrary argument types #4693

Merged

tautschnig force-pushed the autoharness-bounded-slices branch 2 times, most recently from bb14e6f to 91a5837 Compare July 29, 2026 09:18

This was referenced Jul 29, 2026

Autoharness: do not synthesize Arbitrary for structs with reference fields #4694

Merged

Implement Arbitrary for Rc<T> and Arc<T> #4697

Merged

feliperodri added the Z-Autoharness Issue related to autoharness subcommand label Jul 29, 2026

tautschnig mentioned this pull request Jul 29, 2026

Autoharness: support smart pointers of compiler-derivable pointees #4698

Merged

tautschnig mentioned this pull request Aug 5, 2026

Autoharness: constructor-based value generation (--constructor-args) #4717

Merged

feliperodri added this to the Autoharness milestone Aug 18, 2026

tautschnig and others added 3 commits August 21, 2026 22:44

Fix clippy needless_borrow in the summary rendering

5480676

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

feliperodri force-pushed the autoharness-bounded-slices branch from 9466d49 to 5480676 Compare August 22, 2026 01:28

feliperodri approved these changes Aug 22, 2026

View reviewed changes

Comment thread kani-compiler/src/kani_middle/transform/automatic.rs Outdated

feliperodri requested a balanced review from Copilot August 22, 2026 17:42

Copilot started reviewing on behalf of feliperodri August 22, 2026 17:43

View session

Copilot AI reviewed Aug 22, 2026

View reviewed changes

feliperodri requested a balanced review from Copilot August 22, 2026 23:02

Copilot started reviewing on behalf of feliperodri August 22, 2026 23:02

View session

Copilot AI reviewed Aug 22, 2026

View reviewed changes

Comment thread kani-driver/src/autoharness/mod.rs

feliperodri requested a balanced review from Copilot August 22, 2026 23:22

feliperodri enabled auto-merge August 22, 2026 23:22

Copilot started reviewing on behalf of feliperodri August 22, 2026 23:22

View session

Copilot AI reviewed Aug 22, 2026

View reviewed changes

Comment thread kani-compiler/src/kani_middle/transform/automatic.rs

feliperodri disabled auto-merge August 22, 2026 23:26

feliperodri mentioned this pull request Aug 22, 2026

Autoharness: model caller-controlled aliasing between reference/pointer arguments #4750

Open

Autoharness: reference tracking issue model-checking#4750 for cross-a…

016e4ee

…rgument aliasing

feliperodri enabled auto-merge August 22, 2026 23:49

feliperodri added this pull request to the merge queue Aug 23, 2026

feliperodri mentioned this pull request Aug 23, 2026

Autoharness: make --bounded-arguments bounds configurable and surface them in the output #4751

Closed

Merged via the queue into model-checking:main with commit bef93e7 Aug 23, 2026
33 of 34 checks passed

This was referenced Sep 7, 2026

autoharness_analyzer fails on metadata from current Kani model-checking/verify-rust-std#679

Closed

Update autoharness_analyzer for current AutoHarnessSkipReason variants model-checking/verify-rust-std#680

Merged

Navigation Menu

Repository navigation

Autoharness: support slice and string arguments (bounded) - #4691

Autoharness: support slice and string arguments (bounded)#4691
feliperodri merged 8 commits into
model-checking:mainfrom
tautschnig:autoharness-bounded-slices

tautschnig commented Jul 29, 2026 •

edited by feliperodri

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

tautschnig commented Jul 29, 2026 • edited by feliperodri Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description

Testing

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

tautschnig commented Jul 29, 2026 •

edited by feliperodri

Loading