Does symbc support mocking ?

[srgiri]

Hello,
If my understanding is correct, then symbc executes the source code in a custom JVM. So if we mock any method using byte code instrumentation (done on default JVM or operating system's JVM), then symbc cannot see the changes.
Is there any way to inform symbc about the mock methods ?

Example:

public class SUT {
   public int testMethod(int x) {
       int y  = new AnotherClass().makeDouble(x);
       if(y == 2*x)
           return 1;
       else if(y== 3*x)
           return 2;
       else
           return 0;
   }
}


public class AnotherClass {
      public int makeDouble(int i) {
           return 2*i;
      }
}

If I mock the method 'makeDouble()' and return

    return 3*i;

then the test cases would be different.

How symbc handles this scenario ? Please reply.

Regards,
S R Giri

[corinus]

Hi:
You may look at src/classes or peers which define "models" for different classes (and methods). In particular please look at the java.lang.Math models.
Thanks.

[srgiri]

Hi,
Thank you for your response. I will check it.

I have another question.
I think unboxing for wrapper classes is not done in jpf-symbc. I am getting exception for statements as below

    class A {
          List<Integer> lst;
     
         // getter and setter method for lst is here.   
    }
    
    public void testMethod() {
           A a = someMethodReturningObj();
           for(int i=0;i<a.getLst().get(0);i++) {  //getting exception for this line.
                  //do something
            }
     }

Exception:
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodError: ?UNKNOWN?.intValue()I

Could you please guide me how to handle such scenarios. How can I generate test cases for such code. This is very common kind of code we usually see. So need some solution.

Regards,
S R Giri