Module dev.civl.mc
Package dev.civl.mc.state.IF

Interface MemoryUnitFactory

public interface MemoryUnitFactory

  • Method Details

    • add

      void add(MemoryUnitSet muSet, MemoryUnit mu)
      Adds a memory unit to a memory unit set.
      Parameters:
      muSet - the memory unit set which is to be added to a new element
      mu - the memory unit to be added to the given memory unit set

    • add

      void add(MemoryUnitSet muSet, dev.civl.sarl.IF.expr.SymbolicExpression pointer, StateFactory stateFactory)

    • canonic

      MemoryUnitSet canonic(MemoryUnitSet muSet)
      Return the "canonical" version of the given memory unit set. The memory unit set returned will satisfy all of the following:
      • it will be observationally equivalent to the given memory unit set, i.e., there is no way a CIVL-C program can distinguish between the two memory unit sets
      • the memory unit set returned will be the unique representative of its equivalence class, i.e., if this method is invoked with two equivalent memory unit sets, it will return the same object
      Parameters:
      muSet - any non-null memory unit set
      Returns:
      the canonical version of the given memory unit set

    • isJoint

      boolean isJoint(MemoryUnit mu1, MemoryUnit mu2)
      This is an over-approximation method to test if two memory units have any intersection. It returns true if the two memory units may or may NOT have any intersection.
      Parameters:
      mu1 - the first memory unit
      mu2 - the second memory unit
      Returns:

    • isJoint

      boolean isJoint(MemoryUnitSet muSet1, MemoryUnitSet muSet2)
      This is an over-approximation method to test if two memory unit sets have any intersection. It returns true if the two memory unit sets may or may NOT have any intersection.
      Parameters:
      muSet1 - the first memory unit
      muSet2 - the second memory unit
      Returns:

    • isJoint

      boolean isJoint(MemoryUnitSet muSet, MemoryUnit mu)
      This is an over-approximation method of membership testing. If muSet doesn't contain mu, returns false. If muSet may or may not contain mu, returns true.
      Parameters:
      muSet - the memory unit set
      mu - the memory unit to be tested for membership
      Returns:
      false if the given memory unit set does not contain the given memory unit; returns true if it may or may not contain the memory unit.

    • union

      MemoryUnitSet union(MemoryUnitSet muSet1, MemoryUnitSet muSet2)
      This is an over-approximation method of union. It always returns a super set of the union of the given memory unit sets.
      Parameters:
      muSet1 - the first memory unit set
      muSet2 - the second memory unit set
      Returns:

    • intersects

      MemoryUnitSet intersects(MemoryUnitSet muSet1, MemoryUnitSet muSet2)
      This is an over-approximation method of intersection. It always returns a super set of the intersection of the given memory unit sets.
      Parameters:
      muSet1 - the first memory unit set
      muSet2 - the second memory unit set
      Returns:

    • newMemoryUnit

      MemoryUnit newMemoryUnit(int dyscopeID, int varID, dev.civl.sarl.IF.expr.ReferenceExpression reference)

    • newMemoryUnitSet

      MemoryUnitSet newMemoryUnitSet()

    • extendReference

      MemoryUnit extendReference(MemoryUnit mu, dev.civl.sarl.IF.expr.ReferenceExpression extraRef)
      extends a memory unit with extra references. For example, the mu could be an are
      Parameters:
      mu -
      ref -
      Returns:

    • contains

      boolean contains(MemoryUnit mu1, MemoryUnit mu2)
      Does mu1 contains mu2? returns true iff mu1 equals mu2, or mu1 and mu2 are referring to the same object and mu1 is containing mu2.
      Parameters:
      mu1 -
      mu2 -
      Returns: