[ST2017] Lab4: Using JPF(Java Pathfinder) --find and report the division by zero in a program.

The program:

public class Racer implements Runnable {
  int d = 42;
  public void run () {
  doSomething(1001);
  d = 0; // (1)
}

public static void main (String[] args){
  Racer racer = new Racer();
  Thread t = new Thread(racer);
  t.start();
  doSomething(1000);
  int c = 420 / racer.d; // (2)
  System.out.println(c);
}

static void doSomething (int n) {
  try { Thread.sleep(n); } catch (InterruptedException ix) {}
  }
}

通过Hg下载JPF项目:

JPF clone完了.

Eclipse:

菜单栏: Help -> Install new software... ;

Install: Add... :

Ok ;

Next >>> Finish;

/home/ares/文档/Files/jpf 下新建 site.properties 文件, 内容如下:

 

# JPF site configuration  
  
jpf.home = ${user.home}/projects/jpf  
  
# can only expand system properties  
jpf-core = ${user.home}/projects/jpf/jpf-core  
  
# annotation properties extension  
jpf-aprop = ${jpf.home}/jpf-aprop  
extensions+=,${jpf-aprop}  
  
# numeric extension  
jpf-numeric = ${jpf.home}/jpf-numeric  
extensions+=,${jpf-numeric}  
  
# symbolic extension  
jpf-symbc = ${jpf.home}/jpf-symbc  
extensions+=,${jpf-symbc}  
  
# concurrent extension  
#jpf-concurrent = ${jpf.home}/jpf-concurrent  
#extensions+=,${jpf-concurrent}  
  
jpf-shell = ${jpf.home}/jpf-shell  
extensions+=,${jpf-shell}  
  
jpf-awt = ${jpf.home}/jpf-awt  
extensions+=,${jpf-awt}  
  
jpf-awt-shell = ${jpf.home}/jpf-awt-shels  
extensions+=,${jpf-awt-shell}  

菜单栏: Window -> Preferences;

Preferences: JPF Preferences -> Browse...(Path to site.properties), 选择之前建立的文件 /home/ares/文档/Files/jpf/site.properties

JavaPathfinder core system v8.0 (rev 29+) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
Racer.main()

====================================================== search started: 16-5-14 下午1:12
10
10
10

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.ArithmeticException: division by zero
    at Racer.main(Racer.java:13)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:
    at Racer.main(Racer.java:13)


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.ArithmeticException: division by zero  a..."

====================================================== statistics
elapsed time:       00:00:00
states:             new=11,visited=2,backtracked=6,end=3
search:             maxDepth=7,constraints=0
choice generators:  thread=10 (signal=0,lock=1,sharedRef=2,threadApi=3,reschedule=4), data=0
heap:               new=378,released=47,maxLive=357,gcCycles=9
instructions:       3440
max memory:         123MB
loaded code:        classes=66,methods=1502

====================================================== search finished: 17-4-20 下午3:04