Uses of Package
dev.civl.mc.state.IF

Packages that use dev.civl.mc.state.IF

Package	Description
dev.civl.mc.analysis.IF	Module analysis provides a list of analyzers for static/runtime analyzing of a program.
dev.civl.mc.dynamic.IF	Module dynamic provides general computations of symbolic expressions, including the pretty printing method.
dev.civl.mc.kripke.IF	Module kripke provides the definition of various transitions and the enabler and state manager of CIVL.
dev.civl.mc.log.IF	Module log provides the data structure for logging errors during verification.
dev.civl.mc.predicate.IF	Module predicate defines predicates that are required to hold for any CIVL-C programs.
dev.civl.mc.semantics.IF	Module semantics implements the semantics of CIVL-C.
dev.civl.mc.state.IF	Module state is responsible for the creation and manipulation of states of a CIVL model.

Classes in dev.civl.mc.state.IF used by dev.civl.mc.analysis.IF

Class	Description
State	A State represents the (global) state of a CIVL Model.

Classes in dev.civl.mc.state.IF used by dev.civl.mc.dynamic.IF

Class	Description
StateFactory	The state factory is used to create all state objects.

Classes in dev.civl.mc.state.IF used by dev.civl.mc.kripke.IF

Class	Description
MemoryUnitFactory
MemoryUnitSet	A memory unit set represents a set of memory units.
State	A State represents the (global) state of a CIVL Model.
StateFactory	The state factory is used to create all state objects.
UnsatisfiablePathConditionException	Thrown when a path condition becomes unsatisfiable, typically due to a side effect from evaluating an expression.

Classes in dev.civl.mc.state.IF used by dev.civl.mc.log.IF

Class	Description
State	A State represents the (global) state of a CIVL Model.
StateFactory	The state factory is used to create all state objects.
UnsatisfiablePathConditionException	Thrown when a path condition becomes unsatisfiable, typically due to a side effect from evaluating an expression.

Classes in dev.civl.mc.state.IF used by dev.civl.mc.predicate.IF

Class	Description
State	A State represents the (global) state of a CIVL Model.
StateFactory	The state factory is used to create all state objects.

Classes in dev.civl.mc.state.IF used by dev.civl.mc.semantics.IF

Class	Description
MemoryUnit	A memory unit represents an object or a part of an object that can be accessed through an expression, e.g., a[9].x, b[8], c, etc.
MemoryUnitFactory
MemoryUnitSet	A memory unit set represents a set of memory units.
State	A State represents the (global) state of a CIVL Model.
StateFactory	The state factory is used to create all state objects.
UnsatisfiablePathConditionException	Thrown when a path condition becomes unsatisfiable, typically due to a side effect from evaluating an expression.

Classes in dev.civl.mc.state.IF used by dev.civl.mc.state.IF

Class	Description
CIVLHeapException	Extends an execution exception with a state at which error occurred.
CIVLHeapException.HeapErrorKind
CIVLStateException	Extends an execution exception with a state at which error occurred.
DynamicScope	A DynamicScope is a runtime instance of a static scope.
MemoryUnit	A memory unit represents an object or a part of an object that can be accessed through an expression, e.g., a[9].x, b[8], c, etc.
MemoryUnitFactory
MemoryUnitSet	A memory unit set represents a set of memory units.
ProcessState	A ProcessState represents the state of a process (thread of execution) in a CIVL model.
StackEntry	An entry on a call stack of a process; also known as an "activation frame".
State	A State represents the (global) state of a CIVL Model.
StateFactory	The state factory is used to create all state objects.