Invalid handling of ptr offset in switchInt argument (WAS: Large getValue terms) #78
Description
Symptom: long-running requests and large server RAM demands. Leaf states display unevaluated getValue terms (in traversals and nested).
Affected proofs: test_process_initialize_mint_no_freeze and test_process_initialize_mint2_no_freeze
Possibly this is caused by zero-sized data in locals, see runtimeverification/mir-semantics#675 .
The getValue function could be made total and return a dedicated error value to avoid the performance issue and enable more detailed analysis.
A detailed analysis uncovered the root cause of the issue: a switchInt was performed over a singleton array instead of a single element of an array. This array had been created by a pointer offset operation - there is a mistake in the rules for dereferencing pointers with offset.