problem with jdart

[anboua]

when I test test_foo.jpf in " C:\Users\asus\jdart\src\examples\features\simple" test work right ,but when I add a method call myMethod and I test it with test_myMethod.jpf nothing happen, I also try to make an other class java in the other repository "C:\Users\asus\jdart\src\examples\features\test" called Testm.java the problem is :

[SEVERE] cannot load application class features.test.Testm

I tried everything without finding any solution .

this is my site.properties

jpf-core=C:/Users/asus/git/jpf-core jpf-jdart=C:/Users/asus/jdart extensions=${jpf-core},${jpf-symbc}

this is test_myMethod.jpf

@include=./example.jpf

concolic.method=myMethod

this is example.jpf :

@include=../../config/jdart.jpf

target=features.test.Testm

concolic.method.myMethod=features.test.Testm.myMethod(i:int) concolic.method.myMethod.config=all_fields_symbolic

this using.jpf :

@using = jpf-jdart

target=features.test.Testm

method config jdart

concolic.method.myMethod=features.test.Test.myMethod(i:int) concolic.method=myMethod

jpf config

jvm.insn_factory.class=gov.nasa.jpf.jdart.ConcolicInstructionFactory peer_packages=gov.nasa.jpf.jdart.peers; listener=gov.nasa.jpf.jdart.ConcolicListener perturb.class=gov.nasa.jpf.jdart.ConcolicPerturbator search.multiple_errors=true jdart.concolic_explorer_instance=gov.nasa.jpf.jdart.ConcolicExplorer@jdart-explorer

jdart config

symbolic.dp=z3 symbolic.dp.z3.bitvectors=true

logging

log.finest=jdart log.info=constraints

[anboua]

I get a solution , I must run the command "ant" always before testing to get any modification .

[ksluckow]

Can you rephrase what the problem is? The error you were initially seeing ("cannot load application class"), is because your target class features.test.Testm is not on the classpath for jpf. Where is that class located?

[anboua]

the problem that when i forget the command "ant" nothing happen because the command "ant" build the project . if you make any modification in the class or in the method you must run the command "ant" and then /path/to/jpf-core/bin/jpf /path/to/jdart/src/examples/features/simple/test_foo.jpf for example .

[ksluckow]

Yes, you need to recompile your system under test if you make any changes to it.

[anboua]

I am working on a project "automatic annotation for JDart" , I want to know which variables should treat as symbolic , can someone give me a detailed answer in which situation must the variable treat symbolically

2017-03-12 12:53 GMT+01:00 Kasper Luckow notifications@github.com:

Closed #19 https://github.com/psycopaths/jdart/issues/19.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/psycopaths/jdart/issues/19#event-996303593, or mute the thread https://github.com/notifications/unsubscribe-auth/AT-870qsSOCwxwsVzPiXD80CPWxZitY_ks5rk9zFgaJpZM4MZS62 .

[anboua]

can someone help me please ?

[ksluckow]

I believe I already answered your question in issue #6 : It is up to the user to define which inputs to the program should be treated symbolically.