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 <memory-list>;
 
or
 reads <memory-list>;
 
where memory-list is a comma-separated list of expressions of type $memory.
See Also:
  • 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

      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: