Allow extra entry-points to be specified for CI lazy loading

This allows driver programs that want more symbols elaborated
than are strictly accessible from the input arguments to request them.

This makes java-frontend documentation uniform rather than duplicate the
docs as usual, and also makes get_values non-fatal for parameters a
particular frontend did not supply, in common with other getters, in
order to avoid breaking unit tests that don't use lazy-methods.

Author: smowton

regression/cbmc-java/lazyloading10/test.class

@@ -0,0 +1,8 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point test.sety
+^EXIT=6$
+^SIGNAL=0$
+entry point 'test\.sety' is ambiguous between:
+test\.sety:\(I\)V
+test\.sety:\(F\)V

regression/cbmc-java/lazyloading10/test.desc

@@ -0,0 +1,14 @@
+public class test {
+
+    int x;
+    int y;
+    
+    public test() { x = 1; y = 2; }
+    public void setx(int _x) { x = _x; }
+    public void sety(int _y) { y = _y; }
+    public void sety(float _y) { y = (int)_y; }
+    public void f() { }
+    
+}
+
+

regression/cbmc-java/lazyloading10/test.java

@@ -0,0 +1,10 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point "test.sety:(I)V" --lazy-methods-extra-entry-point "test.sety:(F)V"
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+CI lazy methods: elaborate java::test\.sety:\(I\)V
+CI lazy methods: elaborate java::test\.sety:\(F\)V
+--
+CI lazy methods: elaborate java::test\.setx:\(I\)V

regression/cbmc-java/lazyloading11/test.class

@@ -0,0 +1,14 @@
+public class test {
+
+    int x;
+    int y;
+    
+    public test() { x = 1; y = 2; }
+    public void setx(int _x) { x = _x; }
+    public void sety(int _y) { y = _y; }
+    public void sety(float _y) { y = (int)_y; }
+    public void f() { }
+    
+}
+
+

regression/cbmc-java/lazyloading11/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.class
+--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point test.setx
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+CI lazy methods: elaborate java::test\.setx:\(I\)V
+--
+CI lazy methods: elaborate java::test\.sety:\(I\)V
+CI lazy methods: elaborate java::test\.sety:\(F\)V

regression/cbmc-java/lazyloading11/test.java

@@ -0,0 +1,14 @@
+public class test {
+
+    int x;
+    int y;
+    
+    public test() { x = 1; y = 2; }
+    public void setx(int _x) { x = _x; }
+    public void sety(int _y) { y = _y; }
+    public void sety(float _y) { y = (int)_y; }
+    public void f() { }
+    
+}
+
+