Module dev.civl.abc

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

Interface PredicateNode

All Superinterfaces:

ASTNode, BlockItemNode, ContractNode, DeclarationNode, FunctionDeclarationNode, FunctionDefinitionNode, OrdinaryDeclarationNode

public interface PredicateNode
extends ContractNode, FunctionDefinitionNode

The ACSL predicate node, which in the view of ABC, is just a function with a boolean return type. An ACSL predicate annotation will become a function which get inserted in the AST tree at the location of the annotation.

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.statement.BlockItemNode

BlockItemNode.BlockItemKind

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

ContractNode.ContractKind

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

OrdinaryDeclarationNode.OrdinaryDeclarationKind

Method Summary

Modifier and Type	Method	Description
PredicateNode	copy()	Returns a deep copy of this AST node.
ExpressionNode	getExpressionBody()	the body expression of the predicate
SequenceNode<VariableDeclarationNode>	getParameters()	The parameters of the predicate
IdentifierNode	getPredicateName()	The name of the predicate

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.statement.BlockItemNode

blockItemKind

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

contractKind

Methods inherited from interface dev.civl.abc.ast.node.IF.declaration.DeclarationNode

getIdentifier, getName, isDefinition, setEntity, setIdentifier, setIsDefinition

Methods inherited from interface dev.civl.abc.ast.node.IF.declaration.FunctionDeclarationNode

getContract, getEntity, getSystemLibrary, hasAtomicFunctionSpecifier, hasDeviceFunctionSpecifier, hasGlobalFunctionSpecifier, hasInlineFunctionSpecifier, hasNoreturnFunctionSpecifier, hasPureFunctionSpecifier, hasStatefFunctionSpecifier, hasSystemFunctionSpecifier, isLogicFunction, setAtomicFunctionSpecifier, setContract, setDeviceFunctionSpecifier, setGlobalFunctionSpecifier, setInlineFunctionSpecifier, setIsLogicFunction, setNoreturnFunctionSpecifier, setPureFunctionSpecifier, setStatefFunctionSpecifier, setSystemFunctionSpecifier, setSystemLibrary

Methods inherited from interface dev.civl.abc.ast.node.IF.declaration.FunctionDefinitionNode

getBody, getLogicDefinition, getTypeNode, setBody

Methods inherited from interface dev.civl.abc.ast.node.IF.declaration.OrdinaryDeclarationNode

hasExternStorage, hasStaticStorage, ordinaryDeclarationKind, setExternStorage, setStaticStorage, setTypeNode

Method Details

getPredicateName

IdentifierNode getPredicateName()

The name of the predicate

Returns:

getParameters

SequenceNode<VariableDeclarationNode> getParameters()

The parameters of the predicate

Returns:

getExpressionBody

ExpressionNode getExpressionBody()

the body expression of the predicate

Returns:

copy

PredicateNode 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 BlockItemNode

Specified by:

copy in interface ContractNode

Specified by:

copy in interface DeclarationNode

Specified by:

copy in interface FunctionDeclarationNode

Specified by:

copy in interface FunctionDefinitionNode

Specified by:

copy in interface OrdinaryDeclarationNode

Returns:

deep copy of this node