Iterator infrastructure for collection models: snapshot iterators + generic-element annotation

[tautschnig]

Three top-level org.cprover support classes for the collection models' iterator()/enhanced-for support:

• CProverArrayLikeIterator: generic snapshot iterator over an Object[]-backed collection; captures (storage, size) at iterator() time. Top-level rather than an inner class deliberately: a non-static inner class's implicit this$0 creates a Collection <-> Iterator lazy-class-loading cycle that aborts JBMC's nondet initialisation of abstract collection parameters. The class javadoc carries the full design rationale (snapshot-vs-fail-fast trade-off, iteration-order conformance, and the documented opt-in future paths for CME modelling and Iterator.remove()).
• CProverMapEntry<K, V>: read-only snapshot Map.Entry for entrySet() views of parallel-array map models.
• @CProverGenericArrayElement: marks an Object[] field as holding a model class's generic-parameter elements, so JBMC's nondet object factory can specialise the element type.

These are inert until collection models reference them; landing them separately keeps the model changes reviewable.

[Copilot]

Pull request overview

Adds new org.cprover infrastructure types intended to support iterator/enhanced-for modeling in JBMC collection models and to improve nondet initialization of generic-typed Object[] backing arrays.

Changes:

• Introduces CProverArrayLikeIterator<E>: a snapshot iterator over an Object[] + logical size.
• Introduces CProverMapEntry<K,V>: a snapshot/read-only Map.Entry implementation for map entry-set views.
• Introduces @CProverGenericArrayElement: runtime field annotation to mark Object[] fields as holding a model class’s generic-parameter elements.

Reviewed changes

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

File	Description
src/main/java/org/cprover/CProverArrayLikeIterator.java	New snapshot iterator utility for array-backed models (currently not yet wired into existing models).
src/main/java/org/cprover/CProverMapEntry.java	New snapshot Map.Entry implementation for map entry iteration/views.
src/main/java/org/cprover/CProverGenericArrayElement.java	New runtime annotation to convey generic element types for Object[] backing arrays.

---

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