Uses of Package
dev.civl.abc.ast.node.IF.acsl

Packages that use dev.civl.abc.ast.node.IF.acsl

Package	Description
dev.civl.abc.ast.entity.IF	Submodule ast.entity defines entities (objects of type Entity), the abstract things such as types, structures, unions, enumerations, objects (variables), functions, and so on, which can be named by identifiers in a program.
dev.civl.abc.ast.node.IF	Submodule ast.node defines every kind of node in an AST.
dev.civl.abc.ast.node.IF.acsl
dev.civl.abc.ast.node.IF.declaration	The ast.node.declaration submodule defines nodes and other object deadling with declarations in a program.
dev.civl.abc.ast.node.IF.statement	The ast.node.statement submodule defines AST nodes for representing statements in a program.

Classes in dev.civl.abc.ast.node.IF.acsl used by dev.civl.abc.ast.entity.IF

Class	Description
BehaviorNode	This represents a named behavior of the ACSL specification.
ContractNode	A contract node represents an element that may occur in a procedure contract.

Classes in dev.civl.abc.ast.node.IF.acsl used by dev.civl.abc.ast.node.IF

Class	Description
AllocationNode	This represents an ACSL allocation clause, which has the syntax allocates p1, p2, p3; or frees p1, p2, p3;
AnyactNode	This represents ACSL-CIVLC \anyact action to be used in depends contract clauses.
AssignsOrReadsNode	An ACSL assigns or ACSL-CIVLC reads clause specifies a set of existing memory units.
AssumesNode	This represents an ACSL assumes clause, which has the following syntax:
BehaviorNode	This represents a named behavior of the ACSL specification.
CallEventNode	An event that represents a function call with certain arguments, which is a kind of Depends Event.
CompletenessNode	This represents the completeness clause of ACSL, which could be either complete or disjoint
CompositeEventNode	An composite event
CompositeEventNode.EventOperator	The operator of a composite event
ContractNode	A contract node represents an element that may occur in a procedure contract.
DependsEventNode	This represents an event of the depends clause.
DependsNode	A depends clause specifies part of the dependence relation used in partial order reduction (POR).
EnsuresNode	An "ensures" clause in a procedure contract clause that represents a post-condition.
ExtendedQuantifiedExpressionNode	This represents an ACSL extended quantification expression.
ExtendedQuantifiedExpressionNode.ExtendedQuantifier
FocusAssertTransformNode
FocusLoopTransformNode
FocusOrderedTransformNode
GuardsNode	This represents a guards clause that specifies a guard for a function.
InsertTransformNode
InvariantNode
MemoryEventNode	A depends event which specifies reading or writing a list of memory units.
MemoryEventNode.MemoryEventNodeKind
NoactNode	This represents the no-act event \noact, which is an event of depends clauses.
NothingNode	Constant $nothing, argument of $assigns / $reads contract clauses.
ObjectOrRegionOfNode	This represents a $object_of of $region_of expression.
PredicateNode	The ACSL predicate node, which in the view of ABC, is just a function with a boolean return type.
RequiresNode	A requires clause in a CIVL-C procedure contract.
TransformNode

Classes in dev.civl.abc.ast.node.IF.acsl used by dev.civl.abc.ast.node.IF.acsl

Class	Description
AnyactNode	This represents ACSL-CIVLC \anyact action to be used in depends contract clauses.
AssignsOrReadsNode	An ACSL assigns or ACSL-CIVLC reads clause specifies a set of existing memory units.
AssumesNode	This represents an ACSL assumes clause, which has the following syntax:
BehaviorNode	This represents a named behavior of the ACSL specification.
CallEventNode	An event that represents a function call with certain arguments, which is a kind of Depends Event.
CompletenessNode	This represents the completeness clause of ACSL, which could be either complete or disjoint
CompositeEventNode	An composite event
CompositeEventNode.EventOperator	The operator of a composite event
ContractNode	A contract node represents an element that may occur in a procedure contract.
ContractNode.ContractKind	The kinds of contract nodes
DependsEventNode	This represents an event of the depends clause.
DependsEventNode.DependsEventNodeKind
DependsNode	A depends clause specifies part of the dependence relation used in partial order reduction (POR).
EnsuresNode	An "ensures" clause in a procedure contract clause that represents a post-condition.
ExtendedQuantifiedExpressionNode.ExtendedQuantifier
FocusTransformNode
FocusTransformNode.FocusKind
GuardsNode	This represents a guards clause that specifies a guard for a function.
InvariantNode
MemoryEventNode	A depends event which specifies reading or writing a list of memory units.
MemoryEventNode.MemoryEventNodeKind
NoactNode	This represents the no-act event \noact, which is an event of depends clauses.
NothingNode	Constant $nothing, argument of $assigns / $reads contract clauses.
PredicateNode	The ACSL predicate node, which in the view of ABC, is just a function with a boolean return type.
RequiresNode	A requires clause in a CIVL-C procedure contract.
TransformNode

Classes in dev.civl.abc.ast.node.IF.acsl used by dev.civl.abc.ast.node.IF.declaration

Class	Description
ContractNode	A contract node represents an element that may occur in a procedure contract.

Classes in dev.civl.abc.ast.node.IF.acsl used by dev.civl.abc.ast.node.IF.statement

Class	Description
ContractNode	A contract node represents an element that may occur in a procedure contract.