Open srgiri opened 6 years ago
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.
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
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:
If I mock the method 'makeDouble()' and return
then the test cases would be different.
How symbc handles this scenario ? Please reply.
Regards, S R Giri