gov.nasa.jpf.symbc.veritesting

Class VeritestingMain

java.lang.Object

gov.nasa.jpf.symbc.veritesting.VeritestingMain

public class VeritestingMain
extends java.lang.Object

Main class file for veritesting static analysis exploration.

Field Summary

Fields

Modifier and Type	Field and Description
private static java.util.HashSet<java.lang.String>	attemptedMethods
(package private) com.ibm.wala.ssa.SSACFG	cfg
(package private) com.ibm.wala.ipa.cha.ClassHierarchy	cha
(package private) java.lang.String	currentClassName
(package private) java.lang.String	currentMethodName
private java.lang.String	currentPackageName
java.util.HashSet	endingInsnsHash
(package private) com.ibm.wala.ssa.IR	ir
(package private) java.util.HashSet<x10.wala.util.NatLoop>	loops
private boolean	methodAnalysis
(package private) java.lang.String	methodSig
(package private) java.util.HashSet<java.lang.String>	methodSummaryClassNames
(package private) java.util.HashSet<java.lang.String>	methodSummarySubClassNames
static java.util.HashSet<java.lang.String>	skipRegionStrings
static java.util.HashSet<java.lang.String>	skipVeriRegions
(package private) java.util.HashSet	startingPointsHistory
private gov.nasa.jpf.vm.ThreadInfo	ti
static java.util.HashMap<java.lang.String,StaticRegion>	veriRegions

Constructor Summary

Constructors

Constructor and Description
VeritestingMain(gov.nasa.jpf.vm.ThreadInfo ti)

Method Summary

Modifier and Type	Method and Description
void	analyzeForVeritesting(java.util.ArrayList<java.lang.String> classPaths, java.lang.String _className)
static void	findClasses(gov.nasa.jpf.vm.ThreadInfo ti, com.ibm.wala.ipa.cha.ClassHierarchy cha, java.util.ArrayList<java.lang.String> classPaths, java.lang.String startingClassName, java.util.HashSet<java.lang.String> methodSummaryClassNames)
static java.util.HashSet<java.lang.String>	getAttemptedMethods()
private java.lang.String	getPackageName(java.lang.String c)
void	jitAnalyzeForVeritesting(java.util.ArrayList<java.lang.String> classPaths, java.lang.String _className, java.lang.String jvmMethodName, boolean multiPathRegion)
private void	jitStartAnalysis(java.lang.String packageName, java.lang.String className, java.lang.String methodSig, boolean multiPathAnalysis)
private za.ac.sun.cs.green.expr.Operation.Operator	negateOperator(za.ac.sun.cs.green.expr.Operation.Operator operator)
private void	startAnalysis(java.lang.String packageName, java.lang.String className, java.lang.String methodSig)

Methods inherited from class java.lang.Object

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

Field Detail

endingInsnsHash

public java.util.HashSet endingInsnsHash

cha

com.ibm.wala.ipa.cha.ClassHierarchy cha

methodSummaryClassNames

java.util.HashSet<java.lang.String> methodSummaryClassNames

methodSummarySubClassNames

java.util.HashSet<java.lang.String> methodSummarySubClassNames

methodAnalysis

private boolean methodAnalysis

currentPackageName

private java.lang.String currentPackageName

veriRegions

public static java.util.HashMap<java.lang.String,StaticRegion> veriRegions

skipVeriRegions

public static java.util.HashSet<java.lang.String> skipVeriRegions

skipRegionStrings

public static final java.util.HashSet<java.lang.String> skipRegionStrings

ti

private gov.nasa.jpf.vm.ThreadInfo ti

attemptedMethods

private static java.util.HashSet<java.lang.String> attemptedMethods

cfg

com.ibm.wala.ssa.SSACFG cfg

startingPointsHistory

java.util.HashSet startingPointsHistory

currentClassName

java.lang.String currentClassName

currentMethodName

java.lang.String currentMethodName

methodSig

java.lang.String methodSig

loops

java.util.HashSet<x10.wala.util.NatLoop> loops

ir

com.ibm.wala.ssa.IR ir

Constructor Detail

VeritestingMain

public VeritestingMain(gov.nasa.jpf.vm.ThreadInfo ti)

Method Detail

getAttemptedMethods

public static java.util.HashSet<java.lang.String> getAttemptedMethods()

analyzeForVeritesting

public void analyzeForVeritesting(java.util.ArrayList<java.lang.String> classPaths,
                                  java.lang.String _className)

jitStartAnalysis

private void jitStartAnalysis(java.lang.String packageName,
                              java.lang.String className,
                              java.lang.String methodSig,
                              boolean multiPathAnalysis)
                       throws StaticRegionException

Throws:

StaticRegionException

jitAnalyzeForVeritesting

public void jitAnalyzeForVeritesting(java.util.ArrayList<java.lang.String> classPaths,
                                     java.lang.String _className,
                                     java.lang.String jvmMethodName,
                                     boolean multiPathRegion)
                              throws StaticRegionException

Throws:

StaticRegionException

getPackageName

private java.lang.String getPackageName(java.lang.String c)

findClasses

public static void findClasses(gov.nasa.jpf.vm.ThreadInfo ti,
                               com.ibm.wala.ipa.cha.ClassHierarchy cha,
                               java.util.ArrayList<java.lang.String> classPaths,
                               java.lang.String startingClassName,
                               java.util.HashSet<java.lang.String> methodSummaryClassNames)

startAnalysis

private void startAnalysis(java.lang.String packageName,
                           java.lang.String className,
                           java.lang.String methodSig)

negateOperator

private za.ac.sun.cs.green.expr.Operation.Operator negateOperator(za.ac.sun.cs.green.expr.Operation.Operator operator)