Question about how to use JPF to verify some Android app source code

[LesleyDeng]

Respected fellows, 

I'm new to JPF and I'm about to use JPF to verify some Android app source code in Eclipse.

I knew that JPF are not supposed to do checking without test driver, so I created a java class file contains a main method, just like the following:

public class TestDriver {

    public static void main(String[] args) {

    LoginActivity mainAct=new LoginActivity();

    Bundle savedInstanceState=new Bundle();

    mainAct.onCreate(savedInstanceState);

    }

}

and in my .jpf file I wrote like that:

target = com.joelapenna.foursquared.TestDriver

report.console.property_violation=error,trace,snapshot

However, when i run-jpf there was an error message syas:

====================================================== error 1

gov.nasa.jpf.vm.NoUncaughtExceptionsProperty

java.lang.ClassNotFoundException: class not found: android.app.Activity

at com.joelapenna.foursquared.TestDriver.main(com/joelapenna/foursquared/TestDriver.java:9)

I thought it was because the LoginActivity extends Activity and  imports android.app.Activity, so i configure my project's jpf.properties adding the android jar file :

<project>.native_classpath =\

   D:\\Android\\android-sdk\\platforms\\android-15\\android.jar;\

      ${foursquared2}/lib/*.jar

It doesn't work, still the same error message.

Anyone has similar experience? Or knows anything about why such error happens??Thanks.

[guoche...@gmail.com]

try to config  <project>.classpath rather than <project>.native_classpath

在 2015年4月13日星期一 UTC+8上午11:02:57，LesleyDeng写道：