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

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

Package	Description
dev.civl.mc.config.IF	Module config provides static configurations of the CIVL tool.
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.model.IF	Module model defines a static model, i.e., the control flow graph, representation of a CIVL-C program.
dev.civl.mc.model.IF.contract
dev.civl.mc.model.IF.expression	Submodule model.expression defines expression in CIVL.
dev.civl.mc.model.IF.location	Submodule model.location defines a location in the control flow graph of CIVL.
dev.civl.mc.model.IF.statement	Submodule model.statement defines a statement of a CIVL-C program.
dev.civl.mc.model.IF.type	Submodule model.type defines types in CIVL.
dev.civl.mc.model.IF.variable	Submodule model.variable defines variables in CIVL.
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.model.IF used by dev.civl.mc.config.IF

Class	Description
CIVLProperty	Enum class for representing different properties that CIVL checks for.

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

Class	Description
CIVLSource	A CIVLSource object represents a range of text in a source file.
CIVLTypeFactory	The CIVL type factory provides the CIVL primitive types, like $bool, int, float, $scope , etc.
ModelFactory	The factory to create all model components.

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

Class	Description
ModelFactory	The factory to create all model components.

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

Class	Description
CIVLException	Root of CIVL exception hierarchy, representing any kind of event where something goes wrong in CIVL.
CIVLException.Certainty	A certainty level gages how certain we are that this is error is a real error, i.e., not just a spurious error.
CIVLProperty	Enum class for representing different properties that CIVL checks for.
CIVLSource	A CIVLSource object represents a range of text in a source file.

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

Class	Description
AbstractFunction	An abstract function is an uninterpreted mathematical function.
AbstractFunction.SpecialRelationKind	The kind of a special relation represented by this abstract function
CIVLException	Root of CIVL exception hierarchy, representing any kind of event where something goes wrong in CIVL.
CIVLException.Certainty	A certainty level gages how certain we are that this is error is a real error, i.e., not just a spurious error.
CIVLFunction	A CIVL function.
CIVLProperty	Enum class for representing different properties that CIVL checks for.
CIVLSource	A CIVLSource object represents a range of text in a source file.
CIVLTypeFactory	The CIVL type factory provides the CIVL primitive types, like $bool, int, float, $scope , etc.
Fragment	A fragment is a sequence of statements.
Identifier	An identifier.
LogicFunction	A logic function is a function whose definition (body) is either absent (i.e.
Model	A model of a CIVL program.
ModelBuilder	Class to provide translation from an AST to a model.
ModelFactory	The factory to create all model components.
Scope	A scope.
Sourceable
SystemFunction	A system function is a function that is implemented in a library executor, not in source code.

Classes in dev.civl.mc.model.IF used by dev.civl.mc.model.IF.contract

Class	Description
CIVLFunction	A CIVL function.
CIVLSource	A CIVLSource object represents a range of text in a source file.
Scope	A scope.
Sourceable

Classes in dev.civl.mc.model.IF used by dev.civl.mc.model.IF.expression

Class	Description
AbstractFunction	An abstract function is an uninterpreted mathematical function.
CIVLFunction	A CIVL function.
Identifier	An identifier.
Scope	A scope.
Sourceable

Classes in dev.civl.mc.model.IF used by dev.civl.mc.model.IF.location

Class	Description
CIVLFunction	A CIVL function.
Scope	A scope.
Sourceable

Classes in dev.civl.mc.model.IF used by dev.civl.mc.model.IF.statement

Class	Description
CIVLFunction	A CIVL function.
CIVLSource	A CIVLSource object represents a range of text in a source file.
Model	A model of a CIVL program.
Scope	A scope.
Sourceable

Classes in dev.civl.mc.model.IF used by dev.civl.mc.model.IF.type

Class	Description
Identifier	An identifier.
Scope	A scope.

Classes in dev.civl.mc.model.IF used by dev.civl.mc.model.IF.variable

Class	Description
Identifier	An identifier.
Scope	A scope.
Sourceable

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

Class	Description
ModelFactory	The factory to create all model components.

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

Class	Description
CIVLFunction	A CIVL function.
CIVLSource	A CIVLSource object represents a range of text in a source file.
ModelFactory	The factory to create all model components.
Scope	A scope.

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

Class	Description
CIVLException.Certainty	A certainty level gages how certain we are that this is error is a real error, i.e., not just a spurious error.
CIVLFunction	A CIVL function.
CIVLProperty	Enum class for representing different properties that CIVL checks for.
CIVLSource	A CIVLSource object represents a range of text in a source file.
Model	A model of a CIVL program.
ModelFactory	The factory to create all model components.
Scope	A scope.