Module dev.civl.abc

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

Interface AssignsOrReadsNode

All Superinterfaces:

ASTNode, ContractNode

public interface AssignsOrReadsNode
extends ContractNode

An ACSL assigns or ACSL-CIVLC reads clause specifies a set of existing memory units. The claim is that if an existing memory unit is not in the set, it will not be modified in the course of the function call. The syntax is:

 assigns invalid input: '<'memory-list>;
 

or

 reads invalid input: '<'memory-list>;
 

where memory-list is a comma-separated list of expressions of type $memory.

See Also:

• 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
AssignsOrReadsNode	copy()	Returns a deep copy of this AST node.
SequenceNode<ExpressionNode>	getMemoryList()	Gets the list of memory associated with this node.
boolean	isAssigns()	Is this an assigns clause?
boolean	isReads()	Is this a reads 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

getMemoryList

SequenceNode<ExpressionNode> getMemoryList()

Gets the list of memory associated with this node.

Returns:

the list of memory associated with this node.

copy

AssignsOrReadsNode 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

isAssigns

boolean isAssigns()

Is this an assigns clause?

Returns:

isReads

boolean isReads()

Is this a reads clause?

Returns: