Hierarchy For All Packages

Package Hierarchies:

• gov.nasa.jpf.symbc,
• gov.nasa.jpf.symbc.veritesting,
• gov.nasa.jpf.symbc.veritesting.ast.def,
• gov.nasa.jpf.symbc.veritesting.ast.transformations,
• gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess,
• gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen,
• gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop,
• gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment,
• gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess,
• gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants,
• gov.nasa.jpf.symbc.veritesting.ast.transformations.linearization,
• gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns,
• gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases,
• gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst,
• gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution,
• gov.nasa.jpf.symbc.veritesting.ast.transformations.typepropagation,
• gov.nasa.jpf.symbc.veritesting.ast.transformations.Uniquness,
• gov.nasa.jpf.symbc.veritesting.ast.visitors,
• gov.nasa.jpf.symbc.veritesting.ChoiceGenerator,
• gov.nasa.jpf.symbc.veritesting.Heuristics,
• gov.nasa.jpf.symbc.veritesting.VeritestingUtil

Class Hierarchy

• java.lang.Object
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArrayExpressions
  • gov.nasa.jpf.symbc.veritesting.ast.def.ArrayRef
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArraySubscriptMap
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArrayUtil
  • gov.nasa.jpf.symbc.veritesting.ast.def.AssignmentStmt (implements gov.nasa.jpf.symbc.veritesting.ast.def.Stmt)
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenExprVisitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor<T>)
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.AstToGreenVisitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor<T>)
  • gov.nasa.jpf.vm.ChoiceGeneratorBase<T> (implements gov.nasa.jpf.vm.ChoiceGenerator<T>)
    • gov.nasa.jpf.vm.choice.IntIntervalGenerator (implements gov.nasa.jpf.vm.IntChoiceGenerator)
      • gov.nasa.jpf.symbc.numeric.PCChoiceGenerator
        • gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticPCChoiceGenerator
          • gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticBranchChoiceGenerator
  • gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ClassUtils
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.CloneableVarTable<T>
    • gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.FieldRefTypeTable
  • gov.nasa.jpf.symbc.veritesting.ast.def.CompositionStmt (implements gov.nasa.jpf.symbc.veritesting.ast.def.Stmt)
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.CreateStaticRegions
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.DefaultTransformation (implements gov.nasa.jpf.symbc.veritesting.ast.transformations.Transformation)
    • gov.nasa.jpf.symbc.veritesting.ast.transformations.linearization.LinearizationTransformation
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicRegion (implements gov.nasa.jpf.symbc.veritesting.ast.def.Region)
  • za.ac.sun.cs.green.expr.Expression (implements java.lang.Comparable<T>)
    • gov.nasa.jpf.symbc.veritesting.ast.def.IfThenElseExpr
    • za.ac.sun.cs.green.expr.Variable (implements java.io.Serializable)
      • gov.nasa.jpf.symbc.veritesting.ast.def.CloneableVariable (implements java.lang.Cloneable)
        • gov.nasa.jpf.symbc.veritesting.ast.def.ArrayRefVarExpr
        • gov.nasa.jpf.symbc.veritesting.ast.def.AstVarExpr
        • gov.nasa.jpf.symbc.veritesting.ast.def.FieldRefVarExpr
        • gov.nasa.jpf.symbc.veritesting.ast.def.WalaVarExpr
      • gov.nasa.jpf.symbc.veritesting.ast.def.GammaVarExpr
  • gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIdVisitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor<T>)
  • gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprIterVisitor<T> (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor<T>)
    • gov.nasa.jpf.symbc.veritesting.ast.visitors.ForallExprVisitor
      • gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.ValidGreenPredicate
  • gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor<T>)
    • gov.nasa.jpf.symbc.veritesting.ast.visitors.AstIterVisitor<T> (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor<T>)
      • gov.nasa.jpf.symbc.veritesting.ast.visitors.ForallAstVisitor
    • gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor<T>)
      • gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldAccessVisitor
      • gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.FirstITEStmtVisitor
      • gov.nasa.jpf.symbc.veritesting.ast.visitors.FixedPointAstMapVisitor
        • gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.ArraySSAVisitor
        • gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSSAVisitor
        • gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyStmtVisitor
        • gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.SubstitutionVisitor
      • gov.nasa.jpf.symbc.veritesting.ast.transformations.linearization.LinearizationVisitor
      • gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariants.LocalOutputInvariantVisitor
      • gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryVisitor
      • gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionInputVisitor
      • gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionMetricsVisitor
      • gov.nasa.jpf.symbc.veritesting.ast.transformations.typepropagation.TypePropagationVisitor
    • gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.ExprBoundaryVisitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor<T>)
    • gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.ExprRegionInputVisitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor<T>)
    • gov.nasa.jpf.symbc.veritesting.ast.transformations.substitution.ExprSubstitutionVisitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor<T>)
    • gov.nasa.jpf.symbc.veritesting.ast.transformations.typepropagation.ExprTypeVisitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor<T>)
    • gov.nasa.jpf.symbc.veritesting.ast.transformations.Uniquness.ExpUniqueVisitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor<T>)
    • gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.FieldArrayVarToSPFVarVisitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor<T>)
    • gov.nasa.jpf.symbc.veritesting.ast.transformations.constprop.SimplifyRangerExprVisitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor<T>)
  • gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ExprUtil
  • gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitorAdapter<T>
  • gov.nasa.jpf.symbc.veritesting.VeritestingUtil.FailEntry
  • gov.nasa.jpf.symbc.veritesting.ast.def.FieldRef
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.FieldSubscriptMap
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.FindStructuredBlockEndNode
  • gov.nasa.jpf.symbc.veritesting.FixedPointWrapper
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.FlattenStmtListVisitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor<T>)
  • gov.nasa.jpf.GenericProperty (implements java.lang.Cloneable, gov.nasa.jpf.Property)
    • gov.nasa.jpf.PropertyListenerAdapter (implements gov.nasa.jpf.report.PublisherExtension, gov.nasa.jpf.search.SearchListener, gov.nasa.jpf.vm.VMListener)
      • gov.nasa.jpf.symbc.HeuristicListener
      • gov.nasa.jpf.symbc.SymbolicListener (implements gov.nasa.jpf.report.PublisherExtension)
      • gov.nasa.jpf.symbc.SymbolicListener2
      • gov.nasa.jpf.symbc.VeritestingListener (implements gov.nasa.jpf.report.PublisherExtension)
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.arrayaccess.GlobalArraySubscriptMap
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.GlobalSubscriptMap
  • gov.nasa.jpf.symbc.veritesting.Heuristics.HeuristicManager
  • gov.nasa.jpf.symbc.veritesting.ast.def.IfThenElseStmt (implements gov.nasa.jpf.symbc.veritesting.ast.def.Stmt)
  • gov.nasa.jpf.symbc.veritesting.ast.def.Instruction (implements gov.nasa.jpf.symbc.veritesting.ast.def.Stmt)
    • gov.nasa.jpf.symbc.veritesting.ast.def.ArrayLengthInstruction
    • gov.nasa.jpf.symbc.veritesting.ast.def.ArrayLoadInstruction
    • gov.nasa.jpf.symbc.veritesting.ast.def.ArrayStoreInstruction
    • gov.nasa.jpf.symbc.veritesting.ast.def.CheckCastInstruction
    • gov.nasa.jpf.symbc.veritesting.ast.def.GetInstruction
    • gov.nasa.jpf.symbc.veritesting.ast.def.InstanceOfInstruction
    • gov.nasa.jpf.symbc.veritesting.ast.def.InvokeInstruction
    • gov.nasa.jpf.symbc.veritesting.ast.def.NewInstruction
    • gov.nasa.jpf.symbc.veritesting.ast.def.PhiInstruction
    • gov.nasa.jpf.symbc.veritesting.ast.def.PutInstruction
    • gov.nasa.jpf.symbc.veritesting.ast.def.ReturnInstruction
    • gov.nasa.jpf.symbc.veritesting.ast.def.SwitchInstruction
    • gov.nasa.jpf.symbc.veritesting.ast.def.ThrowInstruction
  • gov.nasa.jpf.symbc.veritesting.VeritestingUtil.JITAnalysis
  • gov.nasa.jpf.jvm.JVMInstructionFactory (implements java.lang.Cloneable)
    • gov.nasa.jpf.jvm.bytecode.InstructionFactory
      • gov.nasa.jpf.symbc.SymbolicInstructionFactory
  • gov.nasa.jpf.ListenerAdapter (implements gov.nasa.jpf.report.PublisherExtension, gov.nasa.jpf.search.SearchListener, gov.nasa.jpf.vm.VMListener)
    • gov.nasa.jpf.symbc.GreenListener
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.NoSkipVisitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor<T>)
  • gov.nasa.jpf.symbc.Observations
  • gov.nasa.jpf.symbc.veritesting.VeritestingUtil.Pair<T,V>
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.PhiCondition
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.PhiEdge
  • gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor<T>)
    • gov.nasa.jpf.symbc.veritesting.ast.visitors.StmtPrintVisitor
  • gov.nasa.jpf.symbc.veritesting.ast.visitors.PrettyPrintVisitor.PrettyPrintExpr (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor<T>)
  • gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ReflectUtil
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.RegionBoundaryOutput
  • gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionHitExactHeuristic
  • gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionStatistics
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.RemoveEarlyReturns
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.RemoveEarlyReturns.ReturnResult
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.removeEarlyReturns.ReturnLessVisitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor<T>)
  • gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.SamePathOptimization
  • gov.nasa.jpf.symbc.veritesting.ast.def.SkipStmt (implements gov.nasa.jpf.symbc.veritesting.ast.def.Stmt)
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SPFCaseList
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass1Visitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor<T>)
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor<T>)
  • gov.nasa.jpf.symbc.veritesting.ast.def.SPFCaseStmt (implements gov.nasa.jpf.symbc.veritesting.ast.def.Stmt)
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenExprVisitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor<T>)
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfToGreenVisitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor<T>)
  • gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SpfUtil
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatDefVisitor (implements com.ibm.wala.ssa.SSAInstruction.IVisitor)
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SSAToStatIVisitor (implements com.ibm.wala.ssa.SSAInstruction.IVisitor)
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.SSAUtil
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StackSlotIVisitor (implements com.ibm.wala.ssa.SSAInstruction.IVisitor)
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.StaticRegion (implements gov.nasa.jpf.symbc.veritesting.ast.def.Region)
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTypeIVisitor (implements com.ibm.wala.ssa.SSAInstruction.IVisitor)
  • gov.nasa.jpf.symbc.veritesting.VeritestingUtil.StatisticManager
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.SubscriptPair
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.fieldaccess.SubstituteGetOutput
  • gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SymbCondVisitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor<T>)
  • gov.nasa.jpf.symbc.SymbolicListener.MethodSummary
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.Table<K,V>
    • gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicOutputTable
    • gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.DynamicTable<V>
    • gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTable<V>
      • gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.InputTable
      • gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.OutputTable
      • gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SlotParamTable
      • gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.ValueSymbolTable
      • gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.VarTypeTable
  • java.lang.Throwable (implements java.io.Serializable)
    • java.lang.Exception
      • gov.nasa.jpf.symbc.veritesting.StaticRegionException
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.TransformationData
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.TransformationList (implements gov.nasa.jpf.symbc.veritesting.ast.transformations.Transformation)
  • gov.nasa.jpf.symbc.veritesting.VeritestingUtil.Triple<T,V,K>
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.Uniquness.UniqueRegion
  • gov.nasa.jpf.symbc.veritesting.VeritestingMain
  • za.ac.sun.cs.green.expr.Visitor
    • gov.nasa.jpf.symbc.veritesting.VeritestingUtil.SimplifyGreenVisitor
  • gov.nasa.jpf.symbc.veritesting.VeritestingUtil.WalaUtil
  • gov.nasa.jpf.symbc.veritesting.ast.transformations.AstToGreen.WalaVarToSPFVarVisitor (implements gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor<T>)

Interface Hierarchy

• gov.nasa.jpf.symbc.veritesting.ast.def.Ast
  • gov.nasa.jpf.symbc.veritesting.ast.def.Stmt
• gov.nasa.jpf.symbc.veritesting.ast.visitors.AstVisitor<T>
• gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprVisitor<T>
• gov.nasa.jpf.symbc.veritesting.ast.transformations.Invariant
• gov.nasa.jpf.symbc.veritesting.ast.def.Region
• gov.nasa.jpf.symbc.veritesting.ast.transformations.Transformation

Enum Hierarchy

• java.lang.Object
  • java.lang.Enum<E> (implements java.lang.Comparable<T>, java.io.Serializable)
    • gov.nasa.jpf.symbc.veritesting.Heuristics.PathStatus
    • gov.nasa.jpf.symbc.veritesting.ChoiceGenerator.StaticPCChoiceGenerator.Kind
    • gov.nasa.jpf.symbc.veritesting.StaticRegionException.ExceptionPhase
    • gov.nasa.jpf.symbc.veritesting.FixedPointWrapper.Transformation
    • gov.nasa.jpf.symbc.veritesting.ast.def.SPFCaseStmt.SPFReason
    • gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesInstruction
    • gov.nasa.jpf.symbc.veritesting.VeritestingUtil.FailEntry.FailReason
    • gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.DefUseVisit
    • gov.nasa.jpf.symbc.veritesting.ast.transformations.ssaToAst.PhiCondition.Branch
    • gov.nasa.jpf.symbc.VeritestingListener.VeritestingMode
    • gov.nasa.jpf.symbc.veritesting.VeritestingUtil.ExprUtil.SatResult