Autoharness: support &CStr arguments under --bounded-arguments

[srivatsansamraj]

&str arguments are generated by any_str_ref, which returns the longest valid-UTF-8 prefix of nondeterministic harness-local storage. &CStr had no model and was skipped for a missing Arbitrary implementation: 67 functions on a whole-library verify-std run, 23 of them in core (CStr::to_bytes, to_str, count_bytes, the PartialEq/Ord impls, and so on).

any_c_str_ref follows the same discipline. The last byte of the storage is set to NUL and from_bytes_until_nul returns the bytes before the first one, so the result is a deterministic function of the nondeterministic bytes and satisfies CStr's invariant by construction: no assume, and every C string of length k below the bound arises from storage whose first NUL is at index k. The slice bound applies, less one byte for the NUL. Eligibility and harness generation both go through is_c_str, so they cannot disagree. &mut CStr stays unsupported, as &mut str does.

• any_c_str_ref in kani_core, KaniModel::AnyCStrRef, the Ref arm in autoharness_supported_arg_ty and the matching case in call_kani_any_for_ty.
• cargo_autoharness_c_str, in the shape of cargo_autoharness_slices: reported as requiring the flag without it; with it, a bounds-checked read fails on the empty string, the no-interior-NUL invariant holds, and covers show the empty, the longest and a specific C string are all generated.
• Docs.

Resolves #4803

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

[srivatsansamraj]

The perf-benchcomp failure is inet::checksum::tests::differential, 64 s to 119 s with the same 8,763 VCCs on both sides. Locally that harness takes 72 to 81 s across thirteen runs on main and on this branch, six CaDiCaL rounds every time, and this change only touches autoharness generation, which the perf harnesses do not use. The job's main-side time for this harness has ranged 40 to 148 s over its last fourteen runs (#4822). Could a maintainer re-run the job?