Module dev.civl.abc

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

Interface ContractNode

All Superinterfaces:

ASTNode

All Known Subinterfaces:

AllocationNode, AssignsOrReadsNode, AssumesNode, BehaviorNode, CompletenessNode, DependsNode, EnsuresNode, FocusAssertTransformNode, FocusLoopTransformNode, FocusOrderedTransformNode, FocusTransformNode, GuardsNode, InsertTransformNode, InvariantNode, PredicateNode, RequiresNode, TransformNode

public interface ContractNode
extends ASTNode

A contract node represents an element that may occur in a procedure contract. The procedure contract consists of a sequence of contract nodes.

Nested Class Summary

Nested Classes

Modifier and Type	Interface	Description
static enum	ContractNode.ContractKind	The kinds of contract nodes

Nested classes/interfaces inherited from interface dev.civl.abc.ast.node.IF.ASTNode

ASTNode.NodeKind

Method Summary

Modifier and Type	Method	Description
ContractNode.ContractKind	contractKind()	The kind of this contract node.
ContractNode	copy()	Returns a deep copy of this AST node.

Methods inherited from interface dev.civl.abc.ast.node.IF.ASTNode

addAllTransformAnnotations, addTransformAnnotation, child, childIndex, children, diff, equiv, getAttribute, getOwner, getScope, getSource, id, keepOnly, nextDFS, nodeKind, numChildren, parent, prettyPrint, prettyRepresentation, prettyRepresentation, print, remove, removeChild, removeTransformAnnotation, setAttribute, setChild, setId, setOwner, setScope, toString, transformAnnotations

Method Details

contractKind

ContractNode.ContractKind contractKind()

The kind of this contract node.

Returns:

copy

ContractNode copy()

Description copied from interface: ASTNode

Returns a deep copy of this AST node. The node and all of its descendants will be cloned. The cloning does not copy analysis or attribute information.

Specified by:

copy in interface ASTNode

Returns:

deep copy of this node