need help! cvc3jni not working in eclipse - windows

[Sanik Bajracharya]

Hi Corina/Willem,

I'm trying to run a program under summerschool>loop.java. i did right click on loop.jpf file > Verify and got following error:

java.lang.UnsatisfiedLinkError: no cvc3jni in java.library.path

at java.lang.ClassLoader.loadLibrary(Unknown Source)

at java.lang.Runtime.loadLibrary0(Unknown Source)

at java.lang.System.loadLibrary(Unknown Source)

at cvc3.Embedded.<clinit>(Embedded.java:15)

at gov.nasa.jpf.symbc.numeric.solvers.ProblemCVC3.<init>(ProblemCVC3.java:54)

I have added

 -Djava.library.path= path to my jpf-symbc/lib  

under Arguments and also made sure that enviroment variable LD_LIBRARY_PATH is set to lib.

I tried running by right clicking on loop.jpf > run as > run configurations > selected run-JPF-symbc > clicked on Run. However the error persist.

Please any help would be appreciated.

[Willem Visser]

Are you on a Mac by any chance? Which case you need to set DYLD_LIBRARY_PATH.

[Sanik Bajracharya]

its Windows 7 not Mac

[Quoc-Sang Phan]

If you add lib path to environment variables of Windows then it will
not work.
You need to add lib path to environment variables in the running
configuration of Eclipse.

On Aug 2, 6:12 am, Sanik Bajracharya <sanik.bajracha...@gmail.com>
wrote:

[Sanik Bajracharya]

i have added the environmental variable in eclipse also

run > run configuration> under enviroment variable tab > i have set LD_LIBRARY_PATH to path to jpf-symbc lib path 

but no use , same error

Also i have another question

i have following class layout

class Node{

      Node left, right;

}

class MainApp{

   Node root = null;

   public void run(Node root, Node n1){

if(root != null){

if(this.removeNode(root, n1))

System.out.println("node has been removed");

}

}

public static void main(String[] args) {

TestNode obj = new TestNode();

Node n1 = null;

for(int i=0; i<1 ; i++){

obj.run(obj.root, n1);

}

}

       public boolean removeNode(Node root, Node node){

if(root != null){

Itirator itr = new Itirator(root);

while(itr.hasNext()){

Node current = itr.move();

if(current == node){

current.prev.next = current.next;

return true;

}

}

}

return false;

}

}

Is there a way by help of symbc to populate root object using  using lazy initialization? root could be null or root could have one next, root could have two next and so on to a limit

[Corina Pasareanu]

hey
are you in marktoberdorf?
you do not need cvc3 for that example
just comment out/delete that line and you will use choco instead that should run with no problems
corina

[Corina Pasareanu]

yes sure
look in symbolicheap directory for examples how to run lazy init.
corina

[Sanik Bajracharya]

can't .symbc.sequences.SymbolicSequenceListener go along with lazy initialization settings in .jpf file? I got error following error when trying to add lazy int + symbolic sequence listener

java.lang.ClassCastException: gov.nasa.jpf.symbc.sequences.SequenceChoiceGenerator cannot be cast to gov.nasa.jpf.symbc.heap.HeapChoiceGenerator

at gov.nasa.jpf.symbc.bytecode.ALOAD.execute(ALOAD.java:105)

at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:2223)

at gov.nasa.jpf.jvm.ThreadInfo.executeTransition(ThreadInfo.java:2175)

at gov.nasa.jpf.jvm.SystemState.executeNextTransition(SystemState.java:712)

[Sanik Bajracharya]

what i want to achieve testing is that to test a method that has both string expressions and also the object. I am trying to use symbolic exp for string (by using automata) and object ref(by using lazy init) in the same method. Is this possible?

[manizheh]

Hi
I am facing the same problem when I use cvc3 or Yices as constraint solver ,were you able to solve it?If yes,how?
Thanks.

[Corina Pasareanu]

what is exactly the problem?
can you please send an example?

thanks
corina

--
 
---
You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfind...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.
 
 

[Corina Pasareanu]

i have never tested this.
i think it should be possible.
what is the example?
corina

[manizheh]

Thank you for your attention.
I faced this problem with every example, like:

public int foo(char[] ca) {
        int cnt=0,x=1;
        for(int i=0;i<ca.length-1;i++)
           
                if( ca[i]=='t' && ca[i]==ca[i+1] )
                {
                    if(x/0==1) cnt--;
                    cnt++;
                }
        return cnt;

[Corina Pasareanu]

hi

we can not handle arrays with symbolic length, so for now you would need to pre-allocate the arrya.

can you pls try that?
thanks
corina

[manizheh]

Thanks for your replay.
I think this problem is not related to length of array. I modified code like this and run via these arguments:
+vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory
+vm.classpath=.
+vm.storage.class=
+symbolic.method=foo(sym)
+jpf.report.console.finished=
test1

public class test1 {
    // The method you need tests for

    public int foo(char[] ca) {
       
       
        int cnt=0,x=1;

        for(int i=0;i<3;i++)
          
                if( ca[i]=='t'  )

                {
                    if(x/0==1)
                        cnt--;
                    cnt++;
                }
        return cnt;   
    }
   

    // The test driver

    public static void main(String[] args) {

        test1 mc = new test1();
        char[] ca="symb".toCharArray();
        int x = mc.foo(ca);
        Debug.printPC("\nMyClass1.myMethod Path Condition: ");
    }
}
but problem yet exists.
Indeed, I aim to test my programs via concolic extension in previous versions.  I could run my previous example by Choco ,IAsolver and Coral constraint solver, but the results were not good and  generated test cases didn't cover the code completely, so I decided to examine other constraint solvers, but I' m facing that error for Yices and cvc3. Also I don't know how to use Hampi constraint solver for this.

[Bipro Saha]

Hi:

I am getting following error :

java.lang.UnsatisfiedLinkError: no cvc3jni in java.library.path
    at java.lang.ClassLoader.loadLibrary(Unknown Source)
    at java.lang.Runtime.loadLibrary0(Unknown Source)
    at java.lang.System.loadLibrary(Unknown Source)
    at cvc3.Embedded.<clinit>(Embedded.java:15)
    at gov.nasa.jpf.symbc.numeric.solvers.ProblemCVC3.<init>(ProblemCVC3.java:54)

    at gov.nasa.jpf.symbc.numeric.SymbolicConstraintsGeneral.isSatisfiable(SymbolicConstraintsGeneral.java:89)
    at gov.nasa.jpf.symbc.numeric.PathCondition.simplifyOld(PathCondition.java:338)
    at gov.nasa.jpf.symbc.numeric.PathCondition.simplify(PathCondition.java:271)
    at gov.nasa.jpf.symbc.bytecode.util.IFInstrSymbHelper.getNextInstructionAndSetPCChoice(IFInstrSymbHelper.java:562)
    at gov.nasa.jpf.symbc.bytecode.IF_ICMPGE.execute(IF_ICMPGE.java:47)
    at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1899)
    at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1853)
    at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:738)
    at gov.nasa.jpf.vm.VM.forward(VM.java:1668)
    at gov.nasa.jpf.search.Search.forward(Search.java:579)
    at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:76)
    at gov.nasa.jpf.JPF.run(JPF.java:613)
    at gov.nasa.jpf.JPF.start(JPF.java:190)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
    at java.lang.reflect.Method.invoke(Unknown Source)
    at gov.nasa.jpf.tool.Run.call(Run.java:76)
    at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:117)


I have set up java.library.path to the lib folder of jpf-symbc..But still its not working..

can anyone please help me out?

I am using windows 7...32 bit architecture..


Thanks
Biplab

[Quoc-Sang Phan]

Hi Bipro,

This error means JPF can't find the cvc3 library.

+ If you are running from command line, did you set the environment variable for cvc3?

+ If you are running from Eclipse, did you set the environment variable in the running configuration?

Best wishes,

Sang

[Bipro Saha]

Hi Sang:

I was running from Eclipse, and i also set the environment variable in the running configuration but same error...:(

--

---
You received this message because you are subscribed to a topic in the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/java-pathfinder/_Xt9IcwAtF4/unsubscribe.
To unsubscribe from this group and all its topics, send an email to java-pathfind...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
Biplab Kumar Saha

[Quoc-Sang Phan]

Hi Bipro,

What is the variable that you set?

In Windows, the variable should be PATH, not LD_LIBRARY_PATH as mentioned in the previous posts.

Sang

[Bipro Saha]

Hi Sang:

Yah, i have set the PATH to C:\Users\User\workspace\jpf-symbc\lib.

But still i am facing same error.

Thanks

Bipro

[Quoc-Sang Phan]

Hi Bipro,

It seems you have done all the necessary things, so I don't know where your problem is.

But you can try to print out System.getProperty("java.library.path") before the call to JPF, to verify that the path to cvc3 is included in the library path. 

Best wishes,

Sang