Make pedantic checks in java_verify optional

[atomb]

When java_verify completes execution of a method, it checks the assignments and return values as specified in the JavaSetup block, but also checks that the method has not allocated any new arrays, initialized any new classes, and a number of other things. Sometimes this is desirable behavior, but other times these errors could be downgraded to warnings. We should make it possible to continue execution even if one of these checks fails.

[atomb]

It's now possible to allow allocations with the java_allow_alloc command.

[weaversa]

Will you provide a small example of where to use the command?

[atomb]

This example should cover the basic idea:

https://github.com/GaloisInc/saw-script/blob/master/examples/java/alloc.saw
https://github.com/GaloisInc/saw-script/blob/master/examples/java/Alloc.java

You can see the difference by commenting and uncommenting the java_allow_alloc line.