[kasimte]

Resolves #5022.

-Z valid-value-checks did not report an invalid value read as one element through a slice pointer. A slice [T] carries no static length, so the whole-slice dereference checks no elements, and the indexed read was checked nowhere.

The fix checks the element in the Index/ConstantIndex arm of visit_place when the base is a slice. It fires only on a direct load of the whole element: a reading_value flag (set in visit_operand) restricts the check to Copy/Move operands, and the index must be the last projection. So an address-of, a partial sub-element read, and a nested write are not falsely rejected. A symbolic index makes CBMC cover every element, so no length loop is needed.

A nested invalid sub-element read (e.g. (*p)[i][j]) is still not reported; this matches main, where the Index arm checked nothing.

Testing

tests/expected/valid-value-checks/slice_element.rs: an invalid bool read through *const [bool] fails Invalid value of type `bool` at a concrete and a symbolic index; valid elements, an address-only &raw const borrow, a partial read, and a nested write all verify.

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

[Copilot]

🟡 Changes recommended

Critical validity-checking issues reject valid address-only raw borrows, partial reads, and nested assignments by validating values that are not actually read.

2 open issues

• Avoid validating pointees for address-only raw borrows · New
• Validate only accessed subplaces in slice projections · New

What changed in this PR

This PR addresses #5022 by extending Kani’s -Z valid-value-checks instrumentation to check indexed slice elements, whose validity is not checked by a whole-slice dereference.

Changes:

• Add element validity checks for slice Index and ConstantIndex projections.
• Add regression harnesses for invalid bool reads at concrete and symbolic indices, plus a valid-element control.
• Record expected verification results for all three harnesses.

File	Description
tests/​expected/​valid-value-checks/​slice_element.rs	Adds slice-element validity regression harnesses.
tests/​expected/​valid-value-checks/​slice_element.expected	Specifies two invalid-value failures and one successful verification.
kani-compiler/​src/​kani_middle/​transform/​check_values.rs	Instruments indexed slice elements with validity checks.

_{Review effort: Balanced}