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:
  • 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)
      Parameters:
      isRequirement - true to set this clause to be isRequirement()