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

Enum Class ContractNode.ContractKind

java.lang.Object
java.lang.Enum<ContractNode.ContractKind>
dev.civl.abc.ast.node.IF.acsl.ContractNode.ContractKind
All Implemented Interfaces:
Serializable, Comparable<ContractNode.ContractKind>, Constable
Enclosing interface:
ContractNode
public static enum ContractNode.ContractKind extends Enum<ContractNode.ContractKind>
The kinds of contract nodes

  • Nested Class Summary

    Nested classes/interfaces inherited from class java.lang.Enum

    Enum.EnumDesc<E extends Enum<E>>

  • Enum Constant Summary

    Enum Constants
    Enum Constant
    Description
    ALLOCATES_OR_FREES
    an allocation clause.
    ASSERT
    an ACSL "assert" annotation
    ASSIGNS_READS
    defines memory units assigned by the function
    ASSUMES
    an "assumes" clause
    BEHAVIOR
    An "behavior" node encodes a named behavior block
    COMPLETENESS
    An "completeness" node encodes either a complete or disjoint clause
    DEPENDS
    defines features of the dependent processes of the current one
    ENSURES
    An "ensures" node encodes a post-condition in a procedure contract.
    GUARDS
    A "guard" node represents the guard of a CIVL-C function.
    INVARIANT
    A "invariant" node represents a loop invariant or a general invariant.
    PREDICATE
    ACSL: ANSI/ISO C Specification Language v1.12 section: 2.6.1.
    PURE
    A "pure" node represents the contract for specifying a pure function.
    REQUIRES
    A "requires" node represents a pre-condition in a CIVL-C procedure contract.
    TRANSFORM
    A "transform" node represents a transformation that should be applied to the piece of code annotated by the transform node.

  • Method Summary

    Modifier and Type
    Method
    Description
    static ContractNode.ContractKind
    valueOf(String name)
    Returns the enum constant of this class with the specified name.
    static ContractNode.ContractKind[]
    values()
    Returns an array containing the constants of this enum class, in the order they are declared.

    Methods inherited from class java.lang.Enum

    compareTo, describeConstable, equals, getDeclaringClass, hashCode, name, ordinal, toString, valueOf

    Methods inherited from class java.lang.Object

    getClass, notify, notifyAll, wait, wait, wait

  • Enum Constant Details

    • ALLOCATES_OR_FREES

      public static final ContractNode.ContractKind ALLOCATES_OR_FREES
      an allocation clause. Can be safely cast to AllocationNode.

    • ASSIGNS_READS

      public static final ContractNode.ContractKind ASSIGNS_READS
      defines memory units assigned by the function

    • ASSUMES

      public static final ContractNode.ContractKind ASSUMES
      an "assumes" clause

    • ASSERT

      public static final ContractNode.ContractKind ASSERT
      an ACSL "assert" annotation

    • BEHAVIOR

      public static final ContractNode.ContractKind BEHAVIOR
      An "behavior" node encodes a named behavior block

    • COMPLETENESS

      public static final ContractNode.ContractKind COMPLETENESS
      An "completeness" node encodes either a complete or disjoint clause

    • DEPENDS

      public static final ContractNode.ContractKind DEPENDS
      defines features of the dependent processes of the current one

    • ENSURES

      public static final ContractNode.ContractKind ENSURES
      An "ensures" node encodes a post-condition in a procedure contract. A node of this kind can be safely cast to EnsuresNode.

    • GUARDS

      public static final ContractNode.ContractKind GUARDS
      A "guard" node represents the guard of a CIVL-C function. A node of this kind may be safely cast to
      invalid reference 
      GuardNode
      .

    • INVARIANT

      public static final ContractNode.ContractKind INVARIANT
      A "invariant" node represents a loop invariant or a general invariant.

    • PURE

      public static final ContractNode.ContractKind PURE
      A "pure" node represents the contract for specifying a pure function. A node of this kind may be safely cast to
      invalid reference 
      PureNode
      .

    • REQUIRES

      public static final ContractNode.ContractKind REQUIRES
      A "requires" node represents a pre-condition in a CIVL-C procedure contract. May be safely cast to RequiresNode.

    • TRANSFORM

      public static final ContractNode.ContractKind TRANSFORM
      A "transform" node represents a transformation that should be applied to the piece of code annotated by the transform node.

    • PREDICATE

      public static final ContractNode.ContractKind PREDICATE

      ACSL: ANSI/ISO C Specification Language v1.12 section: 2.6.1.

      A predicate is a boolean value expression

  • Method Details

    • values

      public static ContractNode.ContractKind[] values()
      Returns an array containing the constants of this enum class, in the order they are declared.
      Returns:
      an array containing the constants of this enum class, in the order they are declared

    • valueOf

      public static ContractNode.ContractKind valueOf(String name)
      Returns the enum constant of this class with the specified name. The string must match exactly an identifier used to declare an enum constant in this class. (Extraneous whitespace characters are not permitted.)
      Parameters:
      name - the name of the enum constant to be returned.
      Returns:
      the enum constant with the specified name
      Throws:
      IllegalArgumentException - if this enum class has no constant with the specified name
      NullPointerException - if the argument is null