User Tools

Site Tools


lab4

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 Examples - 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

lab4.1485546205.txt.gz · Last modified: 2017/01/27 19:43 by franck