EECS4315

User Tools

Site Tools

You are here: Mission Critical Systems » Lab 4
Trace:
lab4a

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Next revision		Previous revision
lab4a [2018/01/23 16:10] – created francklab4a [2018/01/23 16:18] (current) – franck
Line 1: Line 1:
 +====== Lab 4 ======
  
- +Implement a listener, named ArrayListener, that counts the number of reads and writes of array cells within the main method of an app.  A sample run can be found below.  It shows what type of output your listener should produce.  Here are some hints that may be useful for implementing your listener. 
-Implement a listener, named ArrayListener, that counts the number of reads and w +  * Consider the interfaces VMListener and SearchListener, which are part of the packages gov.nasa.jpf.vm and gov.nasa.jpf.search, respectively. 
-rites of array cells within the main method of an app.  A sample run can be foun +  * Consider subclasses of the class Instruction, which is part of the package gov.nasa.jpf.vm. 
-d below.  It shows what type of output your listener should produce.  Here are s +  * If you do not know how to count the number of reads and writes of array cells within the main method of an app, then count the number of reads and writes of array cells of the entire app. 
-ome hints that may be useful for implementing your listener. +  * If you do not know how to print the total at the end, then print a star (*) every time a read or write of an array cell occurs.
-<ul> +
-<li> +
-Consider the interfaces VMListener and SearchListener, which are part of the pac +
-kages gov.nasa.jpf.vm and gov.nasa.jpf.search, respectively. +
-<li> +
-Consider subclasses of the class Instruction, which is part of the package gov.n +
-asa.jpf.vm. +
-<li> +
-If you cannot count the number of reads and writes of array cells within the mai +
-n method of an app, then count the number of reads and writes of array cells of  +
-the entire app. +
-<lI> +
-If you cannot print the total at the end, then print a star (*) every time a rea +
-d or write of an array cell occurs. +
-</ul> +
- +
-<p>+
  
 To compile your listener, use To compile your listener, use
-<pre>+<code>
 javac -cp /cs/fac/packages/jpf/jpf-core/build/jpf.jar:. ArrayListener.java javac -cp /cs/fac/packages/jpf/jpf-core/build/jpf.jar:. ArrayListener.java
-</pre> +</code> 
-or add /cs/fac/packages/jpf/jpf-core/build/jpf.jar as an external library to Ecl +or add /cs/fac/packages/jpf/jpf-core/build/jpf.jar as an external library to Eclipse.
-ipse. +
- +
-<p>+
  
 To test your listener, you may want to use the following app. To test your listener, you may want to use the following app.
-<pre> +<code java> 
-public class ArraySample +public class ArraySample { 
-{ +    public static void main(String[] args) {
-    public static void main(String[] args) +
-    {+
         int[] array = new int[2];         int[] array = new int[2];
         array[0] = 1;         array[0] = 1;
Line 45: Line 24:
     }     }
 } }
-</pre>  +</code> 
- +
-<p>+
  
 To run JPF on the above app, use the following configuration file. To run JPF on the above app, use the following configuration file.
-<pre>+<code>
 target=ArraySample target=ArraySample
 classpath=. classpath=.
 listener=ArrayListener listener=ArrayListener
 native_classpath=/eecs/home/franck/ native_classpath=/eecs/home/franck/
-</pre> +</code> 
-where /eecs/home/franck/ is the path to the directory in which ArrayListener.cla +where /eecs/home/franck/ is the path to the directory in which ArrayListener.class can be found.
-ss can be found.+
  
-<p> +If the above configuration file is used with the above app, JPF should produce output similar to the following. 
- +<code> 
-If the above configuration file is used with the above app, JPF should produce o +JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Government. All rights reserved.
-utput similar to the following. +
-<pre> +
-JavaPathfinder core system v8.0 (rev 29) - (C) 2005-2014 United States Governmen +
-t. All rights reserved.+
  
  
Line 71: Line 43:
 ArraySample.main() ArraySample.main()
  
-====================================================== search started: 2/5/17 1: +====================================================== search started: 2/5/17 1:20 PM
-20 PM+
 ***** *****
 Total number of reads and writes of array cells: 6 Total number of reads and writes of array cells: 6
Line 84: Line 55:
 states:             new=1,visited=0,backtracked=1,end=1 states:             new=1,visited=0,backtracked=1,end=1
 search:             maxDepth=1,constraints=0 search:             maxDepth=1,constraints=0
-choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule +choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
-=0), data=0+
 heap:               new=347,released=12,maxLive=0,gcCycles=1 heap:               new=347,released=12,maxLive=0,gcCycles=1
 instructions:       3184 instructions:       3184
Line 91: Line 61:
 loaded code:        classes=60,methods=1320 loaded code:        classes=60,methods=1320
  
-====================================================== search finished: 2/5/17 1 +====================================================== search finished: 2/5/17 1:20 PM 
-:20 PM +</code>
-</pre> +
- +
-<P> +
  
 +To receive feedback, submit your listener using the submit command before Monday February 5:
 submit 4315 lab4 ArrayListener.java submit 4315 lab4 ArrayListener.java
  
  
lab4a.1516723856.txt.gz · Last modified: by franck