Module dev.civl.mc
Package dev.civl.mc.model.IF.type

Interface CIVLType

All Known Subinterfaces:
CIVLArrayType, CIVLBundleType, CIVLCompleteArrayType, CIVLCompleteDomainType, CIVLDomainType, CIVLEnumType, CIVLFunctionType, CIVLHeapType, CIVLMemType, CIVLPointerType, CIVLPrimitiveType, CIVLRegularRangeType, CIVLScopeType, CIVLSetType, CIVLStateType, CIVLStructOrUnionType
public interface CIVLType
Parent of all types.

  • Method Details

    • typeKind

      CIVLType.TypeKind typeKind()

    • hasReferences

      boolean hasReferences()
      Does this type contain a sub-type of pointer or mem type? A value of such a type may contain references to memory locations and those references can be used to read or modify that memory.
      Returns:
      true iff there is a sub-type of this type which is a pointer type or is the "$mem" type.

    • hasState

      boolean hasState()
      If this type contains any array with non-constant extent, it "has state" in the sense that the dynamic type may depend on the state.
      Returns:
      true iff type contains array with non-constant extent

    • getStateVariable

      Variable getStateVariable()
      If a type is defined using a struct, union, or typedef, and it contains state, it may have to be evaluated and stored in a variable of type CIVLDynamicType. For such a type, this method returns the corresponding variable. For other types, it returns null.
      Returns:
      the state variable associated to this type or null

    • setStateVariable

      void setStateVariable(Variable variable)
      Sets this type's state variable to the given variable
      Parameters:
      variable - a variable of type CIVLDynamicType used to store the dynamic type resulting from evaluating this type in a state

    • getDynamicType

      dev.civl.sarl.IF.type.SymbolicType getDynamicType(dev.civl.sarl.IF.SymbolicUniverse universe)
      This returns the dynamic type corresponding to this static type in which all array extent expressions are ignored, i.e., all of the dynamic array types are incomplete. May be null (only in the case of the primitive type of kind
      invalid reference 
      PrimitiveTypeKind.VOID
      ).
      Returns:
      the dynamic type corresponding to this static type with incomplete array type

    • getDynamicTypeIndex

      int getDynamicTypeIndex()
      All dynamic types occurring in a model are indexed. This returns the index of the dynamic type corresponding to this type. CIVL associates a single dynamic type to every CIVL type and does this once at compile time. All the dynamic types which occur as dynamic types of CIVL types are numbered from 0. This is used in particular to construct the bundle type which is the union of all of the dynamic types. This field is the dynamic type index to this one and it's initially be minus one and can be set later by calling
      invalid reference 
      #setDynamicTypeIndex(int)
      and the getter is this method.
      Returns:
      the dynamic type index

    • isNumericType

      boolean isNumericType()
      Returns:
      true iff this type is numeric

    • isIntegerType

      boolean isIntegerType()
      Returns:
      true iff this type is integer type

    • isRealType

      boolean isRealType()
      Returns:
      true iff this type is real type

    • isPointerType

      boolean isPointerType()
      Returns:
      true iff this type is pointer type

    • isProcessType

      boolean isProcessType()
      Returns:
      true iff this type is process type

    • isScopeType

      boolean isScopeType()
      Returns:
      true iff this type is scope type

    • isVoidType

      boolean isVoidType()
      Returns:
      true iff this type is void type

    • isHeapType

      boolean isHeapType()
      Returns:
      true iff this type is heap type

    • isBundleType

      boolean isBundleType()
      Returns:
      true iff this type is bundle type

    • isStructType

      boolean isStructType()
      Returns:
      true iff this type is struct type

    • isUnionType

      boolean isUnionType()
      Returns:
      true iff this type is union type

    • isArrayType

      boolean isArrayType()
      Returns:
      true iff this type is array type

    • isIncompleteArrayType

      boolean isIncompleteArrayType()

    • isCharType

      boolean isCharType()
      Returns:
      true iff this type is char type

    • isRangeType

      boolean isRangeType()
      Returns:
      true iff this type is a CIVLRegularRangeType

    • isSetTypeOf

      boolean isSetTypeOf(CIVLType elementType)
      Parameters:
      elementType - the exptected element type of a CIVLSetType
      Returns:
      true iff this type is a CIVLSetType with element of the given "elementType"

    • isSetType

      boolean isSetType()
      Returns:
      true iff this type is a CIVLSetType with some element type

    • isEnumerationType

      boolean isEnumerationType()
      Returns:
      true iff this type is an enumeration type.

    • isBoolType

      boolean isBoolType()
      Returns:
      true iff this type is a boolean type.

    • isDomainType

      boolean isDomainType()

    • copyAs

      CIVLType copyAs(CIVLPrimitiveType type, dev.civl.sarl.IF.SymbolicUniverse universe)

    • isSuperTypeOf

      boolean isSuperTypeOf(CIVLType subtype)
      Is this type the super type of the given sub-type? If subtype is the same as this type, return true.
      Parameters:
      subtype - The type to be tested if it is the sub-type of this type.
      Returns:

    • isScalar

      boolean isScalar()
      Is this type a scalar type?
      Returns:

    • areSubtypesScalar

      boolean areSubtypesScalar()
      Are all the sub-types of this type scalar?
      Returns:

    • isFunction

      boolean isFunction()

    • freeVariables

      Set<Variable> freeVariables()

    • analyze

      boolean analyze()
      This method should be called after all the types are complete; it analyzes the completed type and caches certain information about them in the instance fields.
      Returns:
      true iff the analysis was successful. The analysis can feel, for example, because a sub-type is incomplete.