spf run example/TestArray.java encounter exception

[idiomaticrefactoring]

Hi:
1: When I run spf examples/TestArray.java it occured exception,details is:

Exception in thread "main" java.lang.UnsatisfiedLinkError: gov.nasa.jpf.symbc.Debug.printPC(Ljava/lang/String;)V
at gov.nasa.jpf.symbc.Debug.printPC(Native Method)

2: But when I Verify TestArray.jpf,it can run.But it can't handle arrList.get(x)_ == 9 and can't generate x<10 [testcase.] How can I know how it handle the library call and How can I look the constraints to help me understand the error

RESULTS is:
Contents of arr:
0 1 2 3 4 5 6 7 8 9 --------->property violated
pc 1 constraint # = 1
x >= 10
=================== Method Sequences
[(expected = java.lang.IndexOutOfBoundsException.class), testarray.testArrayList(10);, ##EXCEPTION## "java.lang.IndexOutOfBoundsException: Index: 0, Size: 10..."]

So am I doing any things wrong? Thank you.


TestArray.jpf:
target=TestArray classpath=${jpf-symbc}/build/examples sourcepath=${jpf-symbc}/src/examples symbolic.method =TestArray.testArrayList(sym) symbolic.min_int=-100 symbolic.max_int=100 #symbolic.dp=z3 #vm.storage.class=nil #listener = .symbc.SymbolicListener #listener = .listener.ChoiceTracker listener = gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener

[R1kM]

Hi,

Regarding your first issue, how are you executing TestArray.java? It seems that you are missing the actual definition of the native method getSolvedPC, can you make sure that Java has access to the JNI methods in peers/gov/nasa/jpf/symbc ?

About the second issue, the range of integers is constrained in the configuration file (TestArray.jpf): you have
symbolic.min_int=-100 symbolic.max_int=100

This tells the solvers to only consider integers in this range. Depending on your needs, you can either increase the range by setting max_int to 1000, and completely remove these constraints.
In any case, you may want to use the option search.multiple_errors=true to instruct SPF not to stop at the first error.

[idiomaticrefactoring]

Hi,
Thank you for your reply. @R1kM

1. I run TestArray.java by Java Application ,so it occured errors.
2. Just as you said,PathCondition x<10 can't generate, because I didn't set the option search.multiple_errors=true.when I did it it occured!

[Xintao-C]

when I run the example TestArray.jpf, I got a error "java.lang.UnsatisfiedLinkError: no libz3java in java.library.path". My computer running environment is Windows 7,JDK 1.8, Is there something wrong with me?