Add Arbitrary impl for char EscapeUnicode

library/kani/src/arbitrary.rs

@@ -71,6 +71,51 @@ impl Arbitrary for std::time::Duration {
     }
 }
 
+impl Arbitrary for std::char::EscapeUnicode {
+    fn any() -> Self {
+        // Generate any state reachable by consuming a freshly constructed
+        // EscapeUnicode iterator from the front.
+        let mut escape = char::any().escape_unicode();
+        let len = escape.len();
+
+        let front = usize::from(u8::any());
+        crate::assume(front <= len);
+
+        if front >= 1 {
+            let _ = escape.next();
+        }
+        if front >= 2 {
+            let _ = escape.next();
+        }
+        if front >= 3 {
+            let _ = escape.next();
+        }
+        if front >= 4 {
+            let _ = escape.next();
+        }
+        if front >= 5 {
+            let _ = escape.next();
+        }
+        if front >= 6 {
+            let _ = escape.next();
+        }
+        if front >= 7 {
+            let _ = escape.next();
+        }
+        if front >= 8 {
+            let _ = escape.next();
+        }
+        if front >= 9 {
+            let _ = escape.next();
+        }
+        if front >= 10 {
+            let _ = escape.next();
+        }
+
+        escape
+    }
+}
+
 /// Generate a slice of *unbounded* nondeterministic length: a fresh allocation of
 /// nondeterministic size whose contents are nondeterministic, with element validity
 /// established by `slice_validity_assume` (a compiler hook that emits a quantified

tests/kani/char_escape_unicode.rs

@@ -0,0 +1,26 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Ensure that `kani::any` can generate valid `std::char::EscapeUnicode` states.
+
+use std::char::EscapeUnicode;
+
+#[kani::proof]
+fn check_arbitrary_escape_unicode() {
+    let escape: EscapeUnicode = kani::any();
+    let count = escape.count();
+
+    assert!(count <= 10);
+
+    kani::cover!(count == 0);
+    kani::cover!(count == 1);
+    kani::cover!(count == 2);
+    kani::cover!(count == 3);
+    kani::cover!(count == 4);
+    kani::cover!(count == 5);
+    kani::cover!(count == 6);
+    kani::cover!(count == 7);
+    kani::cover!(count == 8);
+    kani::cover!(count == 9);
+    kani::cover!(count == 10);
+}

tests/script-based-pre/autoharness_char_escape_unicode/Cargo.toml

@@ -0,0 +1,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "autoharness_char_escape_unicode"
+version = "0.1.0"
+edition = "2024"
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }

tests/script-based-pre/autoharness_char_escape_unicode/config.yml

@@ -0,0 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+script: escape_unicode.sh
+expected: escape_unicode.expected
+exit_code: 0

tests/script-based-pre/autoharness_char_escape_unicode/escape_unicode.expected

@@ -0,0 +1 @@
+| autoharness_char_escape_unicode | consume_escape_unicode | #[kani::proof] | Success |

tests/script-based-pre/autoharness_char_escape_unicode/escape_unicode.sh

@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set -euo pipefail
+
+cargo kani autoharness -Z autoharness --output-format=regular 2>&1 \
+    | grep -E '^\| autoharness_char_escape_unicode \| consume_escape_unicode .*Success' \
+    | tr -s ' '

tests/script-based-pre/autoharness_char_escape_unicode/src/lib.rs

@@ -0,0 +1,8 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#![allow(dead_code)]
+
+pub fn consume_escape_unicode(value: std::char::EscapeUnicode) -> usize {
+    value.count()
+}