Merge pull request #1221 from smowton/smowton/feature/force_load_method

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

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() { }
+    
+}
+
+