Module dev.civl.abc

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

Interface EnsuresNode

All Superinterfaces:

ASTNode, ContractNode

public interface EnsuresNode
extends ContractNode

An "ensures" clause in a procedure contract represents a post-condition.

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
EnsuresNode	copy()	Returns a deep copy of this AST node.
ExpressionNode	getExpression()	An expression of boolean type which is the post-condition
boolean	isGuarantee()
void	setIsGuarantee(boolean isGuarantee)	see isGuarantee()

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()

An expression of boolean type which is the post-condition

Returns:

the boolean expression post-condition

copy

EnsuresNode 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

isGuarantee

boolean isGuarantee()

Returns:

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

setIsGuarantee

void setIsGuarantee(boolean isGuarantee)

see isGuarantee()

Parameters:

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