Module dev.civl.mc

Interface CIVLMemType.MemoryLocationReference

Enclosing interface:
CIVLMemType

public static interface CIVLMemType.MemoryLocationReference
Implementations of CIVLMemType.MemoryLocationReference represent references to a subset of a value of a variable/heap object
  • Method Summary

    Modifier and Type
    Method
    Description
    int
    significant iff isHeapObject()
    boolean
     
    int
    significant iff isHeapObject()
    dev.civl.sarl.IF.expr.SymbolicExpression
    The scope value of the scope where the corresponding variable declared
    dev.civl.sarl.IF.expr.SymbolicExpression
    A CoreUniverse.valueSetTemplate(SymbolicType, ValueSetReference[]) that provides references to sub-values of the variable
    int
    vid()
    The variable ID of the corresponding variable
  • Method Details

    • isHeapObject

      boolean isHeapObject()
      Returns:
      true iff this class represents references to a heap object
    • vid

      int vid()
      The variable ID of the corresponding variable
    • heapID

      int heapID()

      significant iff isHeapObject()

      Returns:
      the ID of a lexical malloc statement which creates the heap object
    • mallocID

      int mallocID()

      significant iff isHeapObject()

      Returns:
      the ID of a run-time call to a lexically specific malloc statement which creates the heap object
    • scopeValue

      dev.civl.sarl.IF.expr.SymbolicExpression scopeValue()
      The scope value of the scope where the corresponding variable declared
    • valueSetTemplate

      dev.civl.sarl.IF.expr.SymbolicExpression valueSetTemplate()
      A CoreUniverse.valueSetTemplate(SymbolicType, ValueSetReference[]) that provides references to sub-values of the variable