Add Arbitrary impl for char EscapeUnicode

[wodex1nhaoIeng]

Description

This PR adds an Arbitrary implementation for std::char::EscapeUnicode.

The implementation generates valid iterator states by starting from an arbitrary char, calling escape_unicode(), and then nondeterministically consuming a valid number of elements from the front. This lets Kani generate reachable EscapeUnicode states without constructing the standard library iterator internals directly.

Motivation

Automatic harness generation needs to synthesize values for function parameters. Functions that take std::char::EscapeUnicode could not be handled because Kani did not know how to generate arbitrary values of that type.

This PR adds direct coverage for kani::any::<std::char::EscapeUnicode>() and a script-based autoharness regression test for a function that takes EscapeUnicode as an argument.

Testing

Ran:

cargo run -p compiletest -- --suite kani --mode kani --force-rerun char_escape_unicode
cargo run -p compiletest -- --suite script-based-pre --mode exec --force-rerun autoharness_char_escape_unicode

[Copilot]

🟢 Approval recommended

The implementation constructively produces valid iterator states and is covered by focused regression tests.

Pull request overview

Adds Arbitrary support for valid, reachable EscapeUnicode iterator states.

Changes:

• Generates states by nondeterministically consuming escaped characters.
• Adds direct and autoharness regression coverage.

File summaries

File	Description
library/kani/src/arbitrary.rs	Implements Arbitrary for EscapeUnicode.
tests/kani/char_escape_unicode.rs	Verifies all possible remaining lengths.
tests/script-based-pre/autoharness_char_escape_unicode/src/lib.rs	Adds an autoharness target.
tests/script-based-pre/autoharness_char_escape_unicode/escape_unicode.sh	Runs and filters the autoharness result.
tests/script-based-pre/autoharness_char_escape_unicode/escape_unicode.expected	Defines expected successful output.
tests/script-based-pre/autoharness_char_escape_unicode/config.yml	Configures the script-based test.
tests/script-based-pre/autoharness_char_escape_unicode/Cargo.toml	Defines the test crate.

Review details

• Files reviewed: 7/7 changed files
• Comments generated: 0
• Review effort level: Balanced

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.