Points-to declarations for arrays in JVMSetup

[brianhuffman]

Currently the JVMSetup blocks used with crucible_jvm_verify only support two specific kinds of points-to declarations:

• jvm_elem_is, for specifying the value of an array element
• jvm_field_is, for specifying the value of an object field

Unlike crucible_llvm_verify, we don't have a way of specifying the value of an entire array at once. This causes a couple of problems, both of which cause serious slowdowns for crucible_jvm_verify:

• Each occurrence of jvm_elem_is turns into a separate proof goal, so it takes n separate prover calls to assert the final value of an array instead of just one
• The fix for issue Array terms are blasted apart and reassembled inefficiently #420 (see Use scVectorReduced when resolving array values in crucible_llvm_verify. #421) that works for crucible_llvm_verify doesn't work for crucible_jvm_verify

Adding a points-to declaration for whole jvm arrays should let us fix both of these problems.