EECS4315

This is an old revision of the document!

---

Choose one of the following listeners (please don't all choose the first one). Write one or more sample programs to illustrate the use of the listener. Some listeners have associated properties. Illustrate their use as well. Describe the listener and its properties. The source code of the listeners can be found in jpf-core/src/main/gov/nasa/jpf/listener/

• gov.nasa.jpf.listener.CoverageAnalyzer
• gov.nasa.jpf.listener.EndlessLoopDetector
• gov.nasa.jpf.listener.InsnCounter
• gov.nasa.jpf.listener.MethodTracker
• gov.nasa.jpf.listener.NoStateCycles
• gov.nasa.jpf.listener.NumericValueChecker
  
  • range.fields=speed,..
  • range.speed.field=x.y.SomeClass.velocity
  • range.speed.min=300
  • range.speed.max=500
  • range.vars=altitude,..
  • range.altitude.var=x.y.SomeClass.computeTrajectory(int):a
  • range.altitude.min=125000
• gov.nasa.jpf.listener.ObjectTracker
  • ot.include
  • ot.exclude
  • ot.refs
  • ot.log_calls
  • ot.log_fields
• gov.nasa.jpf.listener.OOMEInjector
  • oome.locations
  • oome.types
• gov.nasa.jpf.listener.PathOutputMonitor
  • perturb.fields = altitude,…
  • perturb.altitude.field = x.y.MyClass.alt
  • perturb.altitude.class = .perturb.IntOverUnder
  • perturb.altitude.location = MyClass.java:42
  • perturb.altitude.delta = 1
  • perturb.returns = velocity,…
  • perturb.velocity.method = x.y.MyClass.computeVelocity()
  • perturb.velocity.class = .perturb.IntOverUnder
  • perturb.velocity.delta = 50
  • perturb.params = foo, …
  • perturb.foo.method = x.y.MyClass.send(int, float, boolean)
  • perturb.foo.location = MyClass.java:42
  • perturb.class = .perturb.dataAbstractor
• gov.nasa.jpf.listener.ReferenceLocator
  • refloc.create
  • refloc.release
  • refloc.use
• gov.nasa.jpf.listener.SearchStats
• gov.nasa.jpf.listener.StackDepthChecker
  • sdc.max_stack_depth
• gov.nasa.jpf.listener.StackTracker
  • jpf.stack_tracker.log_period
• gov.nasa.jpf.listener.StateCountEstimator
  • jpf.state_count_estimator.log_period
• gov.nasa.jpf.listener.StateTracker
  • jpf.state_tracker.log_period
• gov.nasa.jpf.listener.VarRecorder
  • var_recorder.include
  • var_recorder.exclude
  • var_recorder.fields
  • var_recorder.locals
  • var_recorder.arrays
• gov.nasa.jpf.listener.VarTracker
  • vt.include
  • vt.exclude
  • vt.max_vars
  • vt.methods