Module dev.civl.abc

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

Interface RequiresNode

All Superinterfaces:

ASTNode, ContractNode

public interface RequiresNode
extends ContractNode

A requires clause in a CIVL-C procedure contract. This clause specifies a pre-condition: something that is expected to hold when the function is called.

See Also:

• EnsuresNode
• ContractNode

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
RequiresNode	copy()	Returns a deep copy of this AST node.
ExpressionNode	getExpression()	Gets the boolean condition which is the pre-condition.
boolean	isRequirement()
void	setIsRequirement(boolean isRequirement)	see isRequirement()

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

getExpression

ExpressionNode getExpression()

Gets the boolean condition which is the pre-condition.

Returns:

the boolean expression which specified the pre-condition

copy

RequiresNode 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

isRequirement

boolean isRequirement()

Returns:

true iff this requires clause specifies a "requirement", i.e. a set of absence assertions that is required to be satisfied by any execution of the function specified by this clause.

setIsRequirement

void setIsRequirement(boolean isRequirement)

see isRequirement()

Parameters:

isRequirement - true to set this clause to be isRequirement()