gov.nasa.jpf.symbc.veritesting.ChoiceGenerator

Class SamePathOptimization

java.lang.Object

gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.SamePathOptimization

public class SamePathOptimization
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
(package private) static DynamicRegion	dynRegion
static za.ac.sun.cs.green.expr.Expression	earlyReturnPredicate
(package private) static za.ac.sun.cs.green.expr.Expression	elsePredicate
static boolean	optimizedRegionPath
static boolean	optimizedReturnPath
(package private) static za.ac.sun.cs.green.expr.Expression	regionPredicate
(package private) static za.ac.sun.cs.green.expr.Expression	thenPredicate

Constructor Summary

Constructors

Constructor and Description
SamePathOptimization()

Method Summary

Modifier and Type	Method and Description
private static void	collectPredicates(gov.nasa.jpf.vm.ThreadInfo ti)
static boolean	optimizedChoices(gov.nasa.jpf.vm.ThreadInfo ti, gov.nasa.jpf.vm.Instruction instructionToExecute, StaticBranchChoiceGenerator cg)
static void	runOnSamePath(gov.nasa.jpf.vm.ThreadInfo ti, gov.nasa.jpf.vm.Instruction instructionToExecute, DynamicRegion dynRegion)
static void	runReturnSamePath(gov.nasa.jpf.vm.ThreadInfo ti, gov.nasa.jpf.vm.Instruction instructionToExecute, DynamicRegion dynRegion)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

optimizedRegionPath

public static boolean optimizedRegionPath

optimizedReturnPath

public static boolean optimizedReturnPath

dynRegion

static DynamicRegion dynRegion

regionPredicate

static za.ac.sun.cs.green.expr.Expression regionPredicate

thenPredicate

static za.ac.sun.cs.green.expr.Expression thenPredicate

elsePredicate

static za.ac.sun.cs.green.expr.Expression elsePredicate

earlyReturnPredicate

public static za.ac.sun.cs.green.expr.Expression earlyReturnPredicate

Constructor Detail

SamePathOptimization

public SamePathOptimization()

Method Detail

optimizedChoices

public static boolean optimizedChoices(gov.nasa.jpf.vm.ThreadInfo ti,
                                       gov.nasa.jpf.vm.Instruction instructionToExecute,
                                       StaticBranchChoiceGenerator cg)
                                throws StaticRegionException

Throws:

StaticRegionException

collectPredicates

private static void collectPredicates(gov.nasa.jpf.vm.ThreadInfo ti)
                               throws StaticRegionException

Throws:

StaticRegionException

runOnSamePath

public static void runOnSamePath(gov.nasa.jpf.vm.ThreadInfo ti,
                                 gov.nasa.jpf.vm.Instruction instructionToExecute,
                                 DynamicRegion dynRegion)
                          throws StaticRegionException

Throws:

StaticRegionException

runReturnSamePath

public static void runReturnSamePath(gov.nasa.jpf.vm.ThreadInfo ti,
                                     gov.nasa.jpf.vm.Instruction instructionToExecute,
                                     DynamicRegion dynRegion)
                              throws StaticRegionException

Throws:

StaticRegionException