Module dev.civl.abc

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

Interface MemoryEventNode

All Superinterfaces:

ASTNode, DependsEventNode

public interface MemoryEventNode
extends DependsEventNode

A depends event which specifies reading or writing a list of memory units. It has the syntax

 \read(m0, m1, ...)
 

or

 \write(m0, m1, ...)
 

Nested Class Summary

Nested Classes

Modifier and Type	Interface	Description
static enum	MemoryEventNode.MemoryEventNodeKind

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.DependsEventNode

DependsEventNode.DependsEventNodeKind

Method Summary

Modifier and Type	Method	Description
MemoryEventNode	copy()	Returns a deep copy of this AST node.
SequenceNode<ExpressionNode>	getMemoryList()
boolean	isReach()
boolean	isRead()
boolean	isWrite()
MemoryEventNode.MemoryEventNodeKind	memoryEventKind()

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.DependsEventNode

getEventKind

Method Details

isRead

boolean isRead()

isWrite

boolean isWrite()

isReach

boolean isReach()

memoryEventKind

MemoryEventNode.MemoryEventNodeKind memoryEventKind()

getMemoryList

SequenceNode<ExpressionNode> getMemoryList()

copy

MemoryEventNode 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 DependsEventNode

Returns:

deep copy of this node