Module dev.civl.mc

Interface Variable

All Superinterfaces:
Sourceable

public interface Variable extends Sourceable
A static variable. Each variable is declared in some static scope. Each variable has a name, a type, and an integer variable ID. The ID is in the range [0,n-1], where n is the number of variables in the static scope containing this variable. This variable's ID is unique within its scope.
  • Method Summary

    Modifier and Type
    Method
    Description
    dev.civl.sarl.IF.expr.SymbolicExpression
    returns the constant value of this variable.
    boolean
    returns true iff this variable has some pointer reference, e.g., when the variable is pointer type, or an array of pointer, etc.
    boolean
     
    boolean
     
    boolean
     
    boolean
     
    boolean
    Is this variable declared as a parameter of some function?
    boolean
    is this variable static qualified?
     
    boolean
    return true iff the variable is purely local, i.e., v is purely local if there is no invalid input: '&v' in the model, and in v's scope, if there are no spawned functions that refer to v
     
    void
    setConst(boolean isConst)
     
    void
    setConstantValue(dev.civl.sarl.IF.expr.SymbolicExpression value)
    sets the constant value of this variable
    void
    setIsBound(boolean value)
     
    void
    setIsInput(boolean value)
     
    void
    setIsOutput(boolean value)
     
    void
     
    void
    setPointerRef(boolean value)
    updates the pointer reference feature of this variable.
    void
    setPurelyLocal(boolean value)
    sets this variable to be purely local according to the given value
    void
    setScope(Scope scope)
     
    void
    setStatic(boolean value)
    sets this variable to be static qualified according to the given value
    void
     
    void
    setVid(int vid)
     
     
    int
    vid()
     

    Methods inherited from interface dev.civl.mc.model.IF.Sourceable

    getSource, setCIVLSource
  • Method Details

    • vid

      int vid()
      Returns:
      The index of this variable in the containing scope.
    • type

      CIVLType type()
      Returns:
      The type of this variable.
    • isConst

      boolean isConst()
      Returns:
      Whether this variable is const qualified.
    • isInput

      boolean isInput()
      Returns:
      Whether this variable is input qualified.
    • isOutput

      boolean isOutput()
      Returns:
      Whether this variable is output qualified.
    • isBound

      boolean isBound()
      Returns:
      Whether this variable is a bound variable of a quantified expression.
    • isStatic

      boolean isStatic()
      is this variable static qualified?
      Returns:
    • setType

      void setType(CIVLType type)
      Parameters:
      type - The type of this variable.
    • setConst

      void setConst(boolean isConst)
      Parameters:
      isConst - Whether this variable is a const.
    • setIsInput

      void setIsInput(boolean value)
      Parameters:
      value - Whether this variable is an input.
    • setIsOutput

      void setIsOutput(boolean value)
      Parameters:
      value - Whether this variable is an output.
    • setIsBound

      void setIsBound(boolean value)
      Parameters:
      value - Whether this variable is a bound variable.
    • name

      Identifier name()
      Returns:
      The name of this variable.
    • setName

      void setName(Identifier name)
      Parameters:
      name - The name of this variable.
    • setScope

      void setScope(Scope scope)
      Parameters:
      scope - The scope to which this variable belongs.
    • setVid

      void setVid(int vid)
      Parameters:
      vid - The index of this variable in the containing scope.
    • scope

      Scope scope()
      Returns:
      The scope of this variable.
    • purelyLocal

      boolean purelyLocal()
      return true iff the variable is purely local, i.e., v is purely local if there is no invalid input: '&v' in the model, and in v's scope, if there are no spawned functions that refer to v
      Returns:
    • setPurelyLocal

      void setPurelyLocal(boolean value)
      sets this variable to be purely local according to the given value
      Parameters:
      value -
    • setStatic

      void setStatic(boolean value)
      sets this variable to be static qualified according to the given value
      Parameters:
      value -
    • hasPointerRef

      boolean hasPointerRef()
      returns true iff this variable has some pointer reference, e.g., when the variable is pointer type, or an array of pointer, etc.
      Returns:
    • setPointerRef

      void setPointerRef(boolean value)
      updates the pointer reference feature of this variable. This is for static analysis and is called in the procedure of the containing scope calculating variables with pointer references.
      Parameters:
      value -
    • constantValue

      dev.civl.sarl.IF.expr.SymbolicExpression constantValue()
      returns the constant value of this variable. If the variable is not constant or input qualified, then only
      Returns:
    • setConstantValue

      void setConstantValue(dev.civl.sarl.IF.expr.SymbolicExpression value)
      sets the constant value of this variable
      Parameters:
      value -
    • isParameter

      boolean isParameter()
      Is this variable declared as a parameter of some function?
      Returns:
      true iff this variable is declared as a parameter of some function