Module dev.civl.abc

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

Interface CompletenessNode

All Superinterfaces:

ASTNode, ContractNode

public interface CompletenessNode
extends ContractNode

This represents the completeness clause of ACSL, which could be either complete or disjoint

 complete behaviors (id0, id1, ...)?
 

or *

 disjoint behaviors (id0, id1, ...)?
 

Nested Class Summary

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

ASTNode.NodeKind

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

ContractNode.ContractKind

Method Summary

Modifier and Type	Method	Description
CompletenessNode	copy()	Returns a deep copy of this AST node.
SequenceNode<IdentifierNode>	getIDList()	The list of behavior IDs associates with this completeness clause.
boolean	isComplete()	Is this a complete clause?
boolean	isDisjoint()	Is this a disjoint clause?

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

Methods inherited from interface dev.civl.abc.ast.node.IF.acsl.ContractNode

contractKind

Method Details

getIDList

SequenceNode<IdentifierNode> getIDList()

The list of behavior IDs associates with this completeness clause.

Returns:

copy

CompletenessNode 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

Specified by:

copy in interface ContractNode

Returns:

deep copy of this node

isDisjoint

boolean isDisjoint()

Is this a disjoint clause?

Returns:

isComplete

boolean isComplete()

Is this a complete clause?

Returns: