Hierarchy For All Packages

Package Hierarchies:

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

Class Hierarchy

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

Interface Hierarchy

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

Enum Class Hierarchy

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