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

Interface Location

All Superinterfaces:
Sourceable
public interface Location extends Sourceable
The parent of all locations.

  • Method Details

    • id

      int id()
      Returns:
      The unique ID number of this location.

    • scope

      Scope scope()
      Returns:
      The scope of this location.

    • function

      CIVLFunction function()
      Returns:
      The function containing this location.

    • incoming

      Iterable<Statement> incoming()
      Returns:
      The iterable object of incoming statements.

    • outgoing

      Iterable<Statement> outgoing()
      Returns:
      The iterable object of outgoing statements.

    • getNumOutgoing

      int getNumOutgoing()
      Returns:
      The number of outgoing statements.

    • getNumIncoming

      int getNumIncoming()
      Returns:
      The number of incoming statements.

    • getOutgoing

      Statement getOutgoing(int i)
      Parameters:
      i - index of the statement
      Returns:
      The i'th outgoing statement

    • getIncoming

      Statement getIncoming(int i)
      Parameters:
      i - index of the statement
      Returns:
      The i'th incoming statement

    • getSoleOutgoing

      Statement getSoleOutgoing()
      Returns the sole outgoing statement from this location.
      Returns:
      the outgoing statement
      Throws:
      CIVLInternalException - if the number of outgoing statements from this location is not 1

    • setId

      void setId(int id)
      Set the unique ID number of this location.
      Parameters:
      id - The unique ID number of this location.

    • setScope

      void setScope(Scope scope)
      Parameters:
      scope - The scope of this location.

    • addIncoming

      void addIncoming(Statement statement)
      Parameters:
      statement - A new incoming statement.

    • addOutgoing

      void addOutgoing(Statement statement)
      Parameters:
      statement - A new outgoing statement.

    • print

      void print(String prefix, PrintStream out, boolean isDebug)
      Print this location and all outgoing transitions.
      Parameters:
      prefix - The prefix string for all lines of this printout.
      out - The PrintStream to use for printing this location.
      isDebug - True iff the debugging option is enabled

    • isPurelyLocal

      boolean isPurelyLocal()
      Returns:
      true iff the location is purely local

    • purelyLocalAnalysis

      void purelyLocalAnalysis()
      Analyze if the location is purely local

    • removeOutgoing

      void removeOutgoing(Statement statement)
      Remove a certain outgoing statement
      Parameters:
      statement - The outgoing statement to be removed

    • removeIncoming

      void removeIncoming(Statement statement)
      Remove a certain incoming statement
      Parameters:
      statement - The incoming statement to be removed

    • setEnterAtomic

      void setEnterAtomic()
      This location is the start location of a certain atomic block

    • setLeaveAtomic

      void setLeaveAtomic()
      This location is the end location of a certain atomic block

    • enterAtomic

      boolean enterAtomic()
      Check if the location is entering a general atomic block.
      Returns:
      true iff the location is entering a general atomic block.

    • leaveAtomic

      boolean leaveAtomic()
      Returns:
      true iff the location is leaving a general atomic block

    • atomicKind

      Location.AtomicKind atomicKind()
      Result might be:
      1. NONE: a normal location
      2. ENTER: the start location of an $atomic block
      3. LEAVE: the end location of an $atomic block
      Returns:
      the atomic kind of the location

    • allOutgoingPurelyLocal

      boolean allOutgoingPurelyLocal()
      This is different from isPurelyLocal(), because the latter is more restricted. Because the latter requires the location have exactly one incoming edge in order to avoid loop.
      Returns:
      True iff every outgoing statement is purely local

    • setLoopPossible

      void setLoopPossible(boolean possible)
      During the translation of AST node into CIVL model, it is possible to know if a location with more than one incoming statement possible to be a loop location
      Parameters:
      possible - The value to be used to mark whether this location is possible to be a loop location or not

    • loopAnalysis

      void loopAnalysis()
      Determines whether this location lies on a cycle in which every location has exactly one outgoing statement and that outgoing statement is a NoopStatement, then calls
      invalid reference 
      #setInNoopLoop(boolean)
      with appropriate boolean value.

    • impactScopeOfAtomicOrAtomBlock

      Scope impactScopeOfAtomicOrAtomBlock()
      The impact scope of a location is required in the enabler when an atomic/atom block is encountered, in which case the impact scope of all statements in the atomic block should be considered.
      Returns:

    • setImpactScopeOfAtomicOrAtomBlock

      void setImpactScopeOfAtomicOrAtomBlock(Scope scope)
      set the impact scope of a location, only called when this.AtomicKind == ATOM_ENTER or ATOMIC_ENTER.

    • computeWritableVariables

      void computeWritableVariables(Set<Variable> addressedOfVariables)

    • writableVariables

      Set<Variable> writableVariables()

    • hasDerefs

      boolean hasDerefs()
      This location or some location in the future contains dereferences of some pointers.
      Returns:

    • setAsStart

      void setAsStart(boolean value)

    • isStart

      boolean isStart()
      Returns true if this location is the start location of a function.
      Returns:

    • impactMemUnits

      Set<MemoryUnitExpression> impactMemUnits()
      Returns the impact memory unit expressions of this location.
      Returns:

    • reachableMemUnitsWtPointer

      Set<MemoryUnitExpression> reachableMemUnitsWtPointer()

    • reachableMemUnitsWoPointer

      Set<MemoryUnitExpression> reachableMemUnitsWoPointer()

    • setImpactMemoryUnit

      void setImpactMemoryUnit(Set<MemoryUnitExpression> impacts)

    • setReachableMemUnitsWtPointer

      void setReachableMemUnitsWtPointer(Set<MemoryUnitExpression> reachable)

    • setReachableMemUnitsWoPointer

      void setReachableMemUnitsWoPointer(Set<MemoryUnitExpression> reachable)

    • setSystemCalls

      void setSystemCalls(Set<CallOrSpawnStatement> systemCalls)

    • systemCalls

      Set<CallOrSpawnStatement> systemCalls()

    • hasSpawn

      boolean hasSpawn()
      Is a spawn statement reachable from this location?
      Returns:
      true iff a spawn statement is reachable from this location.

    • staticAnalysis

      void staticAnalysis()

    • setSafeLoop

      void setSafeLoop(boolean value)
      Mark if the loop is a safe loop. For "safe loop", see isSafeLoop()
      Parameters:
      value - True to mark the loop as safe loop; false as may not be a safe loop.

    • isSafeLoop

      boolean isSafeLoop()

      Returns true if this loop satisfies the following conditions:

      1. has one iteration variable
      2. the iteration variable is only modified by the last statement (incremental)
      3. the condition has the form i invalid input: '<' N (or i > N)
      4. the loop has finite iterations (can be decided statically)

      Returns:

    • isGuardedLocation

      boolean isGuardedLocation()
      are the disjunction of the guards of all outgoing statements of this location guarded not TRUE?
      Returns:

    • isInNoopLoop

      boolean isInNoopLoop()
      Determines if this location lies on a cycle in which every location has exactly one outgoing statement and that outgoing statement is a NoopStatement.
      Returns:
      True iff the location is in a cycle in which every location has exactly one outgoing statement and that outgoing statement is a NoopStatement.

    • pathCondition

      Expression pathCondition()
      returns the path condition of this location from the start location
      Returns:

    • setPathcondition

      void setPathcondition(Expression expression)

    • setBinaryBranching

      void setBinaryBranching(boolean value)
      update this location to denote if it is a binary branching location
      Parameters:
      value - the value to be used

    • isBinaryBranching

      boolean isBinaryBranching()
      if this is a location that contains two outgoing statement and the guards are expr and !expr, repectively.
      Returns:

    • setSwitchOrChooseWithDefault

      void setSwitchOrChooseWithDefault()
      Marks this location as a switch or $choose statement location who has a 'default' case. Lets isSwitchOrChooseWithDefault() return true.

    • isSwitchOrChooseWithDefault

      boolean isSwitchOrChooseWithDefault()
      Returns true iff this is a switch or $choose statement location where a set of branch statements emanate from and a default case for it was specified.
      Returns:
      true iff this is a switch or $choose statement location where a set of branch statements emanate from and a default case for it was specified.

    • isInLoop

      boolean isInLoop()
      returns true iff this location has more than one incoming location and is inside a loop.
      Returns:
      true iff this location has more than one incoming location and is inside a loop.

    • isEntryOfUnsafeAtomic

      boolean isEntryOfUnsafeAtomic()
      Returns:
      True iff this location is an atomic block entry and the termination of the atomic block is NOT determined.

    • setEntryOfUnsafeAtomic

      void setEntryOfUnsafeAtomic(boolean unsafe)
      Set the mark of atomic block termination.
      Parameters:
      unsafe - Set to true if this location is an atomic block entry and the termination of the atomic block is NOT determined.

    • isSleep

      boolean isSleep()
      returns true iff this location is the SLEEP location, which has no outgoing statement
      Returns:

    • isEntryOfLocalBlock

      boolean isEntryOfLocalBlock()
      Returns:
      true iff this location is the entry of a local block, i.e., this location is associated with a system function call $local_start

    • setIsEntryOfLocalBlock

      void setIsEntryOfLocalBlock(boolean isEntryOfLocalBlock)
      Parameters:
      isEntryOfLocalBlock - true to mark that this location isEntryOfLocalBlock()