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

Interface Expression

All Superinterfaces:
Sourceable
All Known Subinterfaces:
AbstractFunctionCallExpression, AddressOfExpression, ArrayLambdaExpression, BinaryExpression, BooleanLiteralExpression, BoundVariableExpression, CastExpression, CharLiteralExpression, CompoundLiteralExpression, ConditionalExpression, DereferenceExpression, DerivativeCallExpression, DifferentiableExpression, DomainGuardExpression, DotExpression, DynamicTypeOfExpression, ExtendedQuantifiedExpression, FunctionCallExpression, FunctionGuardExpression, FunctionIdentifierExpression, HereOrRootExpression, InitialValueExpression, IntegerLiteralExpression, LambdaExpression, LHSExpression, LiteralExpression, MemoryUnitExpression, Nothing, ProcnullExpression, QuantifiedExpression, RealLiteralExpression, RecDomainLiteralExpression, RegularRangeExpression, ScopeofExpression, SelfExpression, SizeofExpression, SizeofTypeExpression, StatenullExpression, SubscriptExpression, SystemGuardExpression, UnaryExpression, UndefinedProcessExpression, VariableExpression, WildcardExpression
public interface Expression extends Sourceable
The parent of all expressions.

  • Method Details

    • expressionScope

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

    • lowestScope

      Scope lowestScope()

    • getExpressionType

      CIVLType getExpressionType()
      Returns:
      The type of this expression. For a primitive or variable, this is the type of the primitive or variable. For a cast expression it is the cast type. For operations it is the type of the operation result.

    • expressionKind

      Expression.ExpressionKind expressionKind()
      Returns the kind of this expression
      Returns:
      The expression kind

    • calculateDerefs

      void calculateDerefs()
      Calculate the existence of dereferences in this expression

    • hasDerefs

      boolean hasDerefs()
      return true iff the expression has at least one dereferences of a certain pointer variable
      Returns:
      True of False

    • purelyLocalAnalysisOfVariables

      void purelyLocalAnalysisOfVariables(Scope funcScope)
      Analyzes if variables accessed by this expression are purely local
      Parameters:
      funcScope - The function scope of this expression

    • isPurelyLocal

      boolean isPurelyLocal()
      Returns:
      True iff the expression accessed only purely-local variables

    • purelyLocalAnalysis

      void purelyLocalAnalysis()
      Analyzes if this expression is purely local

    • replaceWith

      void replaceWith(ConditionalExpression oldExpression, VariableExpression newExpression)
      Replace a certain conditional expression with a variable expression. Used when translating away conditional expressions with temporal variable
      Parameters:
      oldExpression - The conditional expression
      newExpression - The variable expression of the temporal variable for the conditional expression

    • replaceWith

      Expression replaceWith(ConditionalExpression oldExpression, Expression newExpression)
      Attempt to create a expression by replacing a certain conditional expression with a new expression, used when translating away conditional expressions without introduction temporal variable
      Parameters:
      oldExpression - The conditional expression
      newExpression - The new expression
      Returns:
      Null if nothing is changed, otherwise the new expression

    • variableAddressedOf

      Set<Variable> variableAddressedOf(Scope scope)
      Compute the set of variables visible from a certain scope that appear in an address-of expression. e.g., (invalid input: '&a' + invalid input: '&b') returns {a} if a is in visible from the given scope while b invisible from the given scope.
      Parameters:
      scope - The scope to focus on.
      Returns:
      a nullable set of variables; null equivalents to an empty set

    • variableAddressedOf

      Set<Variable> variableAddressedOf()
      Compute the set of variables that appear in an address-of expression. e.g., (invalid input: '&a' + invalid input: '&b') returns {a, b}.
      Returns:
      a nullable set of variables; null equivalents to an empty set

    • constantValue

      dev.civl.sarl.IF.expr.SymbolicExpression constantValue()
      The immutable constant value of this expression. NULL if the expression is not a constant.
      Returns:
      the constant value of this expression. NULL if the expression is not a constant.

    • hasConstantValue

      boolean hasConstantValue()
      Checks if this expression has a constant value, i.e., constantValue() != NULL.
      Returns:
      true iff this expression has a constant value.

    • calculateConstantValue

      void calculateConstantValue(dev.civl.sarl.IF.SymbolicUniverse universe)
      Calculates the constant value of this expression.
      Parameters:
      universe - The symbolic universe to be used.

    • containsHere

      boolean containsHere()
      checks if this expression contains the constant $here. e.g.: sinvalid input: '<'$here would return true.
      Returns:

    • setErrorFree

      void setErrorFree(boolean value)

    • isErrorFree

      boolean isErrorFree()
      if this expression is guaranteed to be error-free and thus doesn't need any error checking. e.g., invalid input: '&anon'[0] which is used to translate array literals.
      Returns:

    • freeVariables

      Set<Variable> freeVariables()
      Computes the set of variables which occur freely in this expression. "Free" means not bound, i.e., quantified variables are not included.
      Returns:
      the set of free variables occurring in the expression