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

Interface Statement

All Superinterfaces:
Sourceable
All Known Subinterfaces:
AssignStatement, AtomicLockAssignStatement, CallOrSpawnStatement, CivlParForSpawnStatement, DomainIteratorStatement, LoopBranchStatement, MallocStatement, NoopStatement, ParallelAssignStatement, ReturnStatement, UpdateStatement
public interface Statement extends Sourceable
The parent of all statements.

  • Method Details

    • source

      Location source()
      Returns:
      The location that is the source of this statement.

    • target

      Location target()
      Returns:
      The location that is the target of this statement.

    • guard

      Expression guard()
      Returns:
      The boolean-valued guard expression for this statement.

    • model

      Model model()
      Returns:
      The model to which this statement belongs.

    • setSource

      void setSource(Location source)
      Parameters:
      source - the source to set

    • setTarget

      void setTarget(Location target)
      Parameters:
      target - the target to set

    • setTargetTemp

      void setTargetTemp(Location target)
      updates the target location of this statement, but never add this statement to the incoming set of the target location
      Parameters:
      target - the target to set

    • setSourceTemp

      void setSourceTemp(Location source)
      updates the source location of this statement, but never add this statement to the outgoing set of the source location
      Parameters:
      source - the source to set

    • setGuard

      void setGuard(Expression guard)
      Parameters:
      guard - the guard to set

    • setModel

      void setModel(Model model)
      Parameters:
      model - The Model to which this statement belongs.

    • statementScope

      Scope statementScope()
      Returns:
      The highest scope accessed by this statement. Null if no variables accessed.

    • hasDerefs

      boolean hasDerefs()
      return true iff the statement has at least one dereferences
      Returns:
      True of False

    • calculateDerefs

      void calculateDerefs()
      Calculate if this statement contains any dereference expression

    • purelyLocalAnalysisOfVariables

      void purelyLocalAnalysisOfVariables(Scope funcScope)
      if an invalid input: '&'(var) is encountered, then var is considered as no purely local if a statement inside a function with fscope is accessing some variable that is declared in the scope vscope such that fscope.isDescendantOf(vscope), then that variable is not purely local
      Parameters:
      funcScope - the function scope of the statement

    • isPurelyLocal

      boolean isPurelyLocal()
      Returns:
      True iff the statement accesses only purely-local variables

    • replaceWith

      void replaceWith(ConditionalExpression oldExpression, VariableExpression newExpression)
      Modify this statement including its guard by replacing a certain conditional expression with a variable expression, used when translating away conditional expression and a temporal variable is introduced.
      For example, x = a ? b : c will be translated into if(a) v0 = b; else v0 = c; x = v0;
      Another example, $when(a?b:c) x = k; will be translated into if(a) v0 = b; else v0 = c; $when(v0) x = k;
      Parameters:
      oldExpression - The conditional expression to be cleared.
      newExpression - The variable expression of the temporal variable for the conditional expression.

    • replaceWith

      Statement replaceWith(ConditionalExpression oldExpression, Expression newExpression)
      Return a new statement by copying this statement and modifying it as well as its guard by replacing a certain conditional expression with a expression, used when translating away conditional expression WITHOUT introducing temporary variables. The original statement can't be modified, because it needs to be used twice to generate the if branch statement and the else branch statement.
      For example, x = a ? b : c will be translated into if(a) x = b; else x = c;
      Another example, $when(a?b:c) x = k; will be translated into if(a) $when(b) x=k; else $when(c) x=k;
      Parameters:
      oldExpression - The conditional expression to be cleared.
      newExpression - The new expression to take place of the conditional expression. Usually, it is one of the choice expressions of the conditional expression.
      Returns:
      A new statement without the conditional expression

    • variableAddressedOf

      Set<Variable> variableAddressedOf(Scope scope)
      Obtain the set of variables visible from a certain scope that are possible to be written in the future.
      Parameters:
      scope - The given scope.
      Returns:

    • variableAddressedOf

      Set<Variable> variableAddressedOf()
      Obtain the set of variables whose addresses are referenced.
      Returns:

    • statementKind

      Statement.StatementKind statementKind()
      Obtain the kind of the statement.
      Returns:
      The statement's kind.

    • toStepString

      String toStepString(Location.AtomicKind atomicKind, int atomCount, boolean atomicLockVarChanged)

    • locationStepString

      String locationStepString()
      Get the string representation in the form of: source location id -> target location id e.g. 3 -> 8
      Returns:

    • summaryOfSource

      String summaryOfSource()
      The summary of the source code information of the statement.
      Returns:

    • lowestScope

      Scope lowestScope()
      Obtains the lowest scope of expression accessed by this statement.
      Returns:
      the lowest scope of expression accessed by this statement.

    • calculateConstantValue

      void calculateConstantValue(dev.civl.sarl.IF.SymbolicUniverse universe)

    • reached

      void reached()
      Mark this statement as reached.

    • reachable

      boolean reachable()
      Returns true if the statement has been reached at least once during the verification.
      Returns:

    • setCIVLSource

      void setCIVLSource(CIVLSource source)
      Specified by:
      setCIVLSource in interface Sourceable

    • containsHere

      boolean containsHere()
      checks if the statement (including its guard) contains the constant $here. e.g. (a>0: s=$here) would return true;
      Returns:

    • freeVariables

      Set<Variable> freeVariables()
      Returns all free (not bound) variables that are referenced in this statement.
      Returns:
      the free variables referenced in this statement