Hierarchy For All Packages

Package Hierarchies:

• edu.udel.cis.vsl.civl,
• edu.udel.cis.vsl.civl.analysis.IF,
• edu.udel.cis.vsl.civl.config.IF,
• edu.udel.cis.vsl.civl.dynamic.IF,
• edu.udel.cis.vsl.civl.kripke.IF,
• edu.udel.cis.vsl.civl.log.IF,
• edu.udel.cis.vsl.civl.model.IF,
• edu.udel.cis.vsl.civl.model.IF.contract,
• edu.udel.cis.vsl.civl.model.IF.expression,
• edu.udel.cis.vsl.civl.model.IF.expression.reference,
• edu.udel.cis.vsl.civl.model.IF.location,
• edu.udel.cis.vsl.civl.model.IF.statement,
• edu.udel.cis.vsl.civl.model.IF.type,
• edu.udel.cis.vsl.civl.model.IF.variable,
• edu.udel.cis.vsl.civl.predicate.IF,
• edu.udel.cis.vsl.civl.run.IF,
• edu.udel.cis.vsl.civl.semantics.IF,
• edu.udel.cis.vsl.civl.slice.IF,
• edu.udel.cis.vsl.civl.state.IF,
• edu.udel.cis.vsl.civl.transform.IF,
• edu.udel.cis.vsl.civl.util.IF

Class Hierarchy

• java.lang.Object
  • edu.udel.cis.vsl.civl.analysis.IF.Analysis
  • edu.udel.cis.vsl.civl.semantics.IF.ArrayToolBox.ArrayShape
  • edu.udel.cis.vsl.civl.semantics.IF.ArrayToolBox.ArraySlice
  • edu.udel.cis.vsl.abc.transform.IF.BaseTransformer (implements edu.udel.cis.vsl.abc.transform.IF.Transformer)
    • edu.udel.cis.vsl.civl.transform.IF.ContractTransformer
    • edu.udel.cis.vsl.civl.transform.IF.Cuda2CIVLTransformer
    • edu.udel.cis.vsl.civl.transform.IF.DirectingTransformer
    • edu.udel.cis.vsl.civl.transform.IF.GeneralTransformer
    • edu.udel.cis.vsl.civl.transform.IF.IntOperationTransformer
    • edu.udel.cis.vsl.civl.transform.IF.IOTransformer
    • edu.udel.cis.vsl.civl.transform.IF.LoopContractTransformer
    • edu.udel.cis.vsl.civl.transform.IF.MacroTransformer
    • edu.udel.cis.vsl.civl.transform.IF.MPI2CIVLTransformer
    • edu.udel.cis.vsl.civl.transform.IF.OpenMP2CIVLTransformer
    • edu.udel.cis.vsl.civl.transform.IF.OpenMPOrphanTransformer
    • edu.udel.cis.vsl.civl.transform.IF.OpenMPSimplifier
    • edu.udel.cis.vsl.civl.transform.IF.Pthread2CIVLTransformer
    • edu.udel.cis.vsl.civl.transform.IF.ShortCircuitTransformer
    • edu.udel.cis.vsl.civl.transform.IF.SvcompTransformer
  • edu.udel.cis.vsl.civl.util.IF.BranchConstraints
  • edu.udel.cis.vsl.civl.CIVL
  • edu.udel.cis.vsl.civl.config.IF.CIVLConfiguration
  • edu.udel.cis.vsl.civl.config.IF.CIVLConstants
  • edu.udel.cis.vsl.civl.dynamic.IF.Dynamics
  • edu.udel.cis.vsl.gmc.ErrorLog
    • edu.udel.cis.vsl.civl.log.IF.CIVLErrorLogger
  • edu.udel.cis.vsl.civl.semantics.IF.Evaluation
  • edu.udel.cis.vsl.civl.semantics.IF.Format
  • edu.udel.cis.vsl.civl.kripke.IF.Kripkes
  • edu.udel.cis.vsl.gmc.LogEntry (implements java.lang.Comparable<T>)
    • edu.udel.cis.vsl.civl.log.IF.CIVLLogEntry
  • edu.udel.cis.vsl.civl.model.IF.ModelConfiguration
  • edu.udel.cis.vsl.civl.model.IF.Models
  • edu.udel.cis.vsl.civl.run.IF.ModelTranslator
  • edu.udel.cis.vsl.civl.util.IF.Pair<S,T>
  • edu.udel.cis.vsl.civl.run.IF.Player
    • edu.udel.cis.vsl.civl.run.IF.TracePlayer
    • edu.udel.cis.vsl.civl.run.IF.Verifier
  • edu.udel.cis.vsl.civl.predicate.IF.Predicates
  • edu.udel.cis.vsl.civl.semantics.IF.Semantics
  • edu.udel.cis.vsl.civl.util.IF.Singleton<T> (implements java.lang.Iterable<T>)
  • edu.udel.cis.vsl.gmc.seq.StateManager<STATE,TRANSITION>
    • edu.udel.cis.vsl.civl.kripke.IF.CIVLStateManager
  • edu.udel.cis.vsl.civl.state.IF.States
  • java.lang.Throwable (implements java.io.Serializable)
    • java.lang.Exception
      • edu.udel.cis.vsl.civl.state.IF.CIVLStateException
        • edu.udel.cis.vsl.civl.state.IF.CIVLHeapException
      • edu.udel.cis.vsl.civl.semantics.IF.LibraryLoaderException
      • java.lang.RuntimeException
        • edu.udel.cis.vsl.civl.model.IF.CIVLException
          • edu.udel.cis.vsl.civl.log.IF.CIVLExecutionException
          • edu.udel.cis.vsl.civl.model.IF.CIVLInternalException
          • edu.udel.cis.vsl.civl.model.IF.CIVLSyntaxException
          • edu.udel.cis.vsl.civl.model.IF.CIVLUnimplementedFeatureException
      • edu.udel.cis.vsl.civl.state.IF.UnsatisfiablePathConditionException
  • edu.udel.cis.vsl.civl.transform.IF.TransformerFactory
  • edu.udel.cis.vsl.civl.transform.IF.Transforms
  • edu.udel.cis.vsl.civl.util.IF.Transmuter
  • edu.udel.cis.vsl.civl.util.IF.Triple<R,S,T>
  • edu.udel.cis.vsl.civl.semantics.IF.TypeEvaluation
  • edu.udel.cis.vsl.civl.run.IF.UserInterface
  • edu.udel.cis.vsl.civl.util.IF.Utils

Interface Hierarchy

• edu.udel.cis.vsl.civl.model.IF.AccuracyAssumptionBuilder
• edu.udel.cis.vsl.civl.semantics.IF.ArrayCutter
• edu.udel.cis.vsl.civl.semantics.IF.ArrayReshaper
• edu.udel.cis.vsl.civl.semantics.IF.ArrayToolBox
• edu.udel.cis.vsl.civl.kripke.IF.AtomicStep
• edu.udel.cis.vsl.civl.model.IF.type.CIVLMemType.MemoryLocationReference
• edu.udel.cis.vsl.civl.model.IF.CIVLSource
• edu.udel.cis.vsl.civl.model.IF.type.CIVLType
  • edu.udel.cis.vsl.civl.model.IF.type.CIVLArrayType
    • edu.udel.cis.vsl.civl.model.IF.type.CIVLCompleteArrayType
  • edu.udel.cis.vsl.civl.model.IF.type.CIVLBundleType
  • edu.udel.cis.vsl.civl.model.IF.type.CIVLCompleteDomainType
  • edu.udel.cis.vsl.civl.model.IF.type.CIVLDomainType
  • edu.udel.cis.vsl.civl.model.IF.type.CIVLEnumType
  • edu.udel.cis.vsl.civl.model.IF.type.CIVLFunctionType
  • edu.udel.cis.vsl.civl.model.IF.type.CIVLHeapType
  • edu.udel.cis.vsl.civl.model.IF.type.CIVLPointerType
  • edu.udel.cis.vsl.civl.model.IF.type.CIVLPrimitiveType
    • edu.udel.cis.vsl.civl.model.IF.type.CIVLScopeType
    • edu.udel.cis.vsl.civl.model.IF.type.CIVLStateType
  • edu.udel.cis.vsl.civl.model.IF.type.CIVLSetType
    • edu.udel.cis.vsl.civl.model.IF.type.CIVLMemType
    • edu.udel.cis.vsl.civl.model.IF.type.CIVLRegularRangeType (also extends edu.udel.cis.vsl.civl.model.IF.type.CIVLStructOrUnionType)
  • edu.udel.cis.vsl.civl.model.IF.type.CIVLStructOrUnionType
    • edu.udel.cis.vsl.civl.model.IF.type.CIVLRegularRangeType (also extends edu.udel.cis.vsl.civl.model.IF.type.CIVLSetType)
• edu.udel.cis.vsl.civl.model.IF.CIVLTypeFactory
• edu.udel.cis.vsl.civl.analysis.IF.CodeAnalyzer
• edu.udel.cis.vsl.civl.run.IF.CommandLine
• edu.udel.cis.vsl.civl.model.IF.contract.ContractFactory
• edu.udel.cis.vsl.civl.slice.IF.DominatorAnalysis<E>
• edu.udel.cis.vsl.civl.dynamic.IF.DynamicMemoryLocationSet
• edu.udel.cis.vsl.civl.dynamic.IF.DynamicMemoryLocationSetFactory
• edu.udel.cis.vsl.civl.state.IF.DynamicScope
• edu.udel.cis.vsl.gmc.seq.EnablerIF<STATE,TRANSITION>
  • edu.udel.cis.vsl.civl.kripke.IF.Enabler
• edu.udel.cis.vsl.civl.semantics.IF.Evaluator
• edu.udel.cis.vsl.civl.semantics.IF.Executor
• edu.udel.cis.vsl.civl.model.IF.Fragment
• java.lang.Iterable<T>
  • edu.udel.cis.vsl.civl.state.IF.MemoryUnitSet
• edu.udel.cis.vsl.civl.kripke.IF.LibraryEnabler
• edu.udel.cis.vsl.civl.kripke.IF.LibraryEnablerLoader
• edu.udel.cis.vsl.civl.semantics.IF.LibraryEvaluator
• edu.udel.cis.vsl.civl.semantics.IF.LibraryEvaluatorLoader
• edu.udel.cis.vsl.civl.semantics.IF.LibraryExecutor
• edu.udel.cis.vsl.civl.semantics.IF.LibraryExecutorLoader
• edu.udel.cis.vsl.civl.state.IF.MemoryUnit
• edu.udel.cis.vsl.civl.semantics.IF.MemoryUnitExpressionEvaluator
• edu.udel.cis.vsl.civl.state.IF.MemoryUnitFactory
• edu.udel.cis.vsl.civl.model.IF.expression.reference.MemoryUnitReference
  • edu.udel.cis.vsl.civl.model.IF.expression.reference.ArraySliceReference
  • edu.udel.cis.vsl.civl.model.IF.expression.reference.SelfReference
  • edu.udel.cis.vsl.civl.model.IF.expression.reference.StructOrUnionFieldReference
• edu.udel.cis.vsl.civl.model.IF.ModelBuilder
• edu.udel.cis.vsl.civl.model.IF.ModelFactory
• edu.udel.cis.vsl.civl.util.IF.Printable
• edu.udel.cis.vsl.civl.state.IF.ProcessState
• edu.udel.cis.vsl.civl.slice.IF.Slice
• edu.udel.cis.vsl.civl.model.IF.Sourceable
  • edu.udel.cis.vsl.civl.model.IF.CIVLFunction
    • edu.udel.cis.vsl.civl.model.IF.AbstractFunction
    • edu.udel.cis.vsl.civl.model.IF.LogicFunction
    • edu.udel.cis.vsl.civl.model.IF.SystemFunction
  • edu.udel.cis.vsl.civl.model.IF.contract.DependsEvent
    • edu.udel.cis.vsl.civl.model.IF.contract.CallEvent
    • edu.udel.cis.vsl.civl.model.IF.contract.CompositeEvent
    • edu.udel.cis.vsl.civl.model.IF.contract.MemoryEvent
  • edu.udel.cis.vsl.civl.model.IF.expression.Expression
    • edu.udel.cis.vsl.civl.model.IF.expression.AbstractFunctionCallExpression
      • edu.udel.cis.vsl.civl.model.IF.expression.DerivativeCallExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.AddressOfExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.ArrayLambdaExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.BinaryExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.BoundVariableExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.CastExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.ConditionalExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.DifferentiableExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.DomainGuardExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.DynamicTypeOfExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.ExtendedQuantifiedExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.FunctionCallExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.FunctionGuardExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.FunctionIdentifierExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.HereOrRootExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.InitialValueExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.LambdaExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.LHSExpression
      • edu.udel.cis.vsl.civl.model.IF.expression.DereferenceExpression
      • edu.udel.cis.vsl.civl.model.IF.expression.DotExpression
      • edu.udel.cis.vsl.civl.model.IF.expression.SubscriptExpression
      • edu.udel.cis.vsl.civl.model.IF.expression.VariableExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.LiteralExpression
      • edu.udel.cis.vsl.civl.model.IF.expression.ArrayLiteralExpression
      • edu.udel.cis.vsl.civl.model.IF.expression.BooleanLiteralExpression
      • edu.udel.cis.vsl.civl.model.IF.expression.CharLiteralExpression
      • edu.udel.cis.vsl.civl.model.IF.expression.IntegerLiteralExpression
      • edu.udel.cis.vsl.civl.model.IF.expression.RealLiteralExpression
      • edu.udel.cis.vsl.civl.model.IF.expression.RecDomainLiteralExpression
      • edu.udel.cis.vsl.civl.model.IF.expression.StructOrUnionLiteralExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.MemoryUnitExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.MPIContractExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.Nothing
    • edu.udel.cis.vsl.civl.model.IF.expression.ProcnullExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.QuantifiedExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.RegularRangeExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.ScopeofExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.SelfExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.SizeofExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.SizeofTypeExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.StatenullExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.SystemGuardExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.UnaryExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.UndefinedProcessExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.ValueAtExpression
    • edu.udel.cis.vsl.civl.model.IF.expression.WildcardExpression
  • edu.udel.cis.vsl.civl.model.IF.contract.FunctionBehavior
    • edu.udel.cis.vsl.civl.model.IF.contract.MPICollectiveBehavior
    • edu.udel.cis.vsl.civl.model.IF.contract.NamedFunctionBehavior
  • edu.udel.cis.vsl.civl.model.IF.contract.FunctionContract
  • edu.udel.cis.vsl.civl.model.IF.Identifier
  • edu.udel.cis.vsl.civl.model.IF.location.Location
  • edu.udel.cis.vsl.civl.model.IF.contract.LoopContract
  • edu.udel.cis.vsl.civl.model.IF.Model
  • edu.udel.cis.vsl.civl.model.IF.Scope
  • edu.udel.cis.vsl.civl.model.IF.statement.Statement
    • edu.udel.cis.vsl.civl.model.IF.statement.AssignStatement
    • edu.udel.cis.vsl.civl.model.IF.statement.AtomicLockAssignStatement
    • edu.udel.cis.vsl.civl.model.IF.statement.CallOrSpawnStatement
    • edu.udel.cis.vsl.civl.model.IF.statement.CivlParForSpawnStatement
    • edu.udel.cis.vsl.civl.model.IF.statement.DomainIteratorStatement
    • edu.udel.cis.vsl.civl.model.IF.statement.MallocStatement
    • edu.udel.cis.vsl.civl.model.IF.statement.NoopStatement
      • edu.udel.cis.vsl.civl.model.IF.statement.LoopBranchStatement
    • edu.udel.cis.vsl.civl.model.IF.statement.ParallelAssignStatement
    • edu.udel.cis.vsl.civl.model.IF.statement.ReturnStatement
    • edu.udel.cis.vsl.civl.model.IF.statement.UpdateStatement
    • edu.udel.cis.vsl.civl.model.IF.statement.WithStatement
  • edu.udel.cis.vsl.civl.model.IF.variable.Variable
• edu.udel.cis.vsl.civl.state.IF.StackEntry
• edu.udel.cis.vsl.civl.state.IF.State
• edu.udel.cis.vsl.civl.state.IF.StateFactory
• edu.udel.cis.vsl.gmc.StatePredicateIF<S>
  • edu.udel.cis.vsl.civl.predicate.IF.CIVLStatePredicate
    • edu.udel.cis.vsl.civl.predicate.IF.AndPredicate
    • edu.udel.cis.vsl.civl.predicate.IF.Deadlock
    • edu.udel.cis.vsl.civl.predicate.IF.FunctionalEquivalence
    • edu.udel.cis.vsl.civl.predicate.IF.PotentialDeadlock
    • edu.udel.cis.vsl.civl.predicate.IF.TrivialPredicate
• edu.udel.cis.vsl.civl.state.IF.StateValueHelper
• edu.udel.cis.vsl.civl.model.IF.type.StructOrUnionField
• edu.udel.cis.vsl.civl.semantics.IF.SymbolicAnalyzer
• edu.udel.cis.vsl.civl.dynamic.IF.SymbolicUtility
• edu.udel.cis.vsl.gmc.TraceStepIF<STATE>
  • edu.udel.cis.vsl.civl.kripke.IF.TraceStep
• edu.udel.cis.vsl.civl.semantics.IF.Transition

Enum Hierarchy

• java.lang.Object
  • java.lang.Enum<E> (implements java.lang.Comparable<T>, java.io.Serializable)
    • edu.udel.cis.vsl.civl.model.IF.expression.reference.ArraySliceReference.ArraySliceKind
    • edu.udel.cis.vsl.civl.model.IF.expression.BinaryExpression.BINARY_OPERATOR
    • edu.udel.cis.vsl.civl.config.IF.CIVLConstants.DeadlockKind
    • edu.udel.cis.vsl.civl.config.IF.CIVLConstants.ErrorStateEquivalence
    • edu.udel.cis.vsl.civl.model.IF.CIVLException.Certainty
    • edu.udel.cis.vsl.civl.model.IF.CIVLException.ErrorKind
    • edu.udel.cis.vsl.civl.state.IF.CIVLHeapException.HeapErrorKind
    • edu.udel.cis.vsl.civl.model.IF.type.CIVLPrimitiveType.PrimitiveTypeKind
    • edu.udel.cis.vsl.civl.model.IF.type.CIVLType.TypeKind
    • edu.udel.cis.vsl.civl.run.IF.CommandLine.CommandLineKind
    • edu.udel.cis.vsl.civl.run.IF.CommandLine.CommandName
    • edu.udel.cis.vsl.civl.model.IF.contract.CompositeEvent.CompositeEventOperator
    • edu.udel.cis.vsl.civl.model.IF.contract.DependsEvent.DependsEventKind
    • edu.udel.cis.vsl.civl.model.IF.expression.Expression.ExpressionKind
    • edu.udel.cis.vsl.civl.semantics.IF.Format.ConversionType
    • edu.udel.cis.vsl.civl.model.IF.contract.FunctionContract.ContractKind
    • edu.udel.cis.vsl.civl.model.IF.expression.LHSExpression.LHSExpressionKind
    • edu.udel.cis.vsl.civl.model.IF.expression.LiteralExpression.LiteralKind
    • edu.udel.cis.vsl.civl.model.IF.location.Location.AtomicKind
    • edu.udel.cis.vsl.civl.model.IF.expression.reference.MemoryUnitReference.MemoryUnitReferenceKind
    • edu.udel.cis.vsl.civl.model.IF.contract.MPICollectiveBehavior.MPICommunicationPattern
    • edu.udel.cis.vsl.civl.model.IF.expression.MPIContractExpression.MPI_CONTRACT_EXPRESSION_KIND
    • edu.udel.cis.vsl.civl.model.IF.statement.NoopStatement.NoopKind
    • edu.udel.cis.vsl.civl.model.IF.expression.QuantifiedExpression.Quantifier
    • edu.udel.cis.vsl.civl.model.IF.statement.Statement.StatementKind
    • edu.udel.cis.vsl.civl.semantics.IF.Transition.AtomicLockAction
    • edu.udel.cis.vsl.civl.semantics.IF.Transition.TransitionKind
    • edu.udel.cis.vsl.civl.model.IF.expression.UnaryExpression.UNARY_OPERATOR
    • edu.udel.cis.vsl.civl.util.IF.Utils.Color