Uses of Interface
dev.civl.abc.ast.node.IF.acsl.ContractNode

Packages that use ContractNode

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.

Uses of ContractNode in dev.civl.abc.ast.entity.IF

Methods in dev.civl.abc.ast.entity.IF that return types with arguments of type ContractNode

Modifier and Type	Method	Description
Iterable<ContractNode>	Function.getContracts()	Returns a Iterator for a set of contract clauses.

Methods in dev.civl.abc.ast.entity.IF with parameters of type ContractNode

Modifier and Type	Method	Description
void	Function.addContract(ContractNode contract)	Add a ContractNode which represents a contract clause.

Uses of ContractNode in dev.civl.abc.ast.node.IF

Method parameters in dev.civl.abc.ast.node.IF with type arguments of type ContractNode

Modifier and Type	Method	Description
AbstractFunctionDefinitionNode	NodeFactory.newAbstractFunctionDefinitionNode(Source source, IdentifierNode name, TypeNode type, SequenceNode<ContractNode> contract, int continuity, SequenceNode<PairNode<ExpressionNode,ExpressionNode>> intervals, StringLiteralNode attr)	Creates a new CIVL abstract function definition.
BehaviorNode	NodeFactory.newBehaviorNode(Source source, IdentifierNode name, SequenceNode<ContractNode> body)	creates a behavior node.
CivlForNode	NodeFactory.newCivlForNode(Source source, boolean isParallel, DeclarationListNode variables, ExpressionNode domain, StatementNode body, SequenceNode<ContractNode> loopContract)	Creates a new instance of the CIVL $for or $parfor node.
LoopNode	NodeFactory.newDoLoopNode(Source source, ExpressionNode condition, StatementNode body, SequenceNode<ContractNode> contracts)	Constructs a new node representing a do...while loop.
ForLoopNode	NodeFactory.newForLoopNode(Source source, ForLoopInitializerNode initializer, ExpressionNode condition, ExpressionNode incrementer, StatementNode body, SequenceNode<ContractNode> contracts)	Constructs a new for loop node.
FunctionDeclarationNode	NodeFactory.newFunctionDeclarationNode(Source source, IdentifierNode name, TypeNode type, SequenceNode<ContractNode> contract)	Creates a new function declaration with no body (so it is not a function "definition").
FunctionDefinitionNode	NodeFactory.newFunctionDefinitionNode(Source source, IdentifierNode name, FunctionTypeNode type, SequenceNode<ContractNode> contract, CompoundStatementNode body)	Constructs a new node representing a function definition, i.e., a function declaration with body.
LoopNode	NodeFactory.newWhileLoopNode(Source source, ExpressionNode condition, StatementNode body, SequenceNode<ContractNode> contracts)	Constructs a new node representing a while loop.

Uses of ContractNode in dev.civl.abc.ast.node.IF.acsl

Subinterfaces of ContractNode in dev.civl.abc.ast.node.IF.acsl

Modifier and Type	Interface	Description
interface	AllocationNode	This represents an ACSL allocation clause, which has the syntax allocates p1, p2, p3; or frees p1, p2, p3;
interface	AssignsOrReadsNode	An ACSL assigns or ACSL-CIVLC reads clause specifies a set of existing memory units.
interface	AssumesNode	This represents an ACSL assumes clause, which has the following syntax:
interface	BehaviorNode	This represents a named behavior of the ACSL specification.
interface	CompletenessNode	This represents the completeness clause of ACSL, which could be either complete or disjoint
interface	DependsNode	A depends clause specifies part of the dependence relation used in partial order reduction (POR).
interface	EnsuresNode	An "ensures" clause in a procedure contract clause that represents a post-condition.
interface	FocusAssertTransformNode
interface	FocusLoopTransformNode
interface	FocusOrderedTransformNode
interface	FocusTransformNode
interface	GuardsNode	This represents a guards clause that specifies a guard for a function.
interface	InsertTransformNode
interface	InvariantNode
interface	PredicateNode	The ACSL predicate node, which in the view of ABC, is just a function with a boolean return type.
interface	RequiresNode	A requires clause in a CIVL-C procedure contract.
interface	TransformNode

Methods in dev.civl.abc.ast.node.IF.acsl that return ContractNode

Modifier and Type	Method	Description
ContractNode	ContractNode.copy()

Methods in dev.civl.abc.ast.node.IF.acsl that return types with arguments of type ContractNode

Modifier and Type	Method	Description
SequenceNode<ContractNode>	BehaviorNode.getBody()	returns the body of this behavior, which is a sequence of contract nodes

Uses of ContractNode in dev.civl.abc.ast.node.IF.declaration

Methods in dev.civl.abc.ast.node.IF.declaration that return types with arguments of type ContractNode

Modifier and Type	Method	Description
SequenceNode<ContractNode>	FunctionDeclarationNode.getContract()	Returns the contract node for this function declaration.

Method parameters in dev.civl.abc.ast.node.IF.declaration with type arguments of type ContractNode

Modifier and Type	Method	Description
void	FunctionDeclarationNode.setContract(SequenceNode<ContractNode> contract)	Sets the contract node child of this node to the given node.

Uses of ContractNode in dev.civl.abc.ast.node.IF.statement

Methods in dev.civl.abc.ast.node.IF.statement that return types with arguments of type ContractNode

Modifier and Type	Method	Description
SequenceNode<ContractNode>	CivlForNode.loopContracts()	Optional loop contracts node.
SequenceNode<ContractNode>	LoopNode.loopContracts()