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

Interface CIVLFunction

All Superinterfaces:
Sourceable
All Known Subinterfaces:
AbstractFunction, LogicFunction, SystemFunction
public interface CIVLFunction extends Sourceable
A CIVL function.

  • Method Details

    • isNondet

      boolean isNondet()

    • name

      Identifier name()
      Returns:
      The name of this function.

    • fid

      int fid()
      The id of this function in its containing scope
      Returns:
      the id of this function

    • parameters

      List<Variable> parameters()
      Returns:
      The list of parameters.

    • returnType

      CIVLType returnType()
      Returns:
      The return type of this function.

    • scopes

      Set<Scope> scopes()
      Returns:
      The set of scopes in this function.

    • outerScope

      Scope outerScope()
      Returns:
      The outermost local scope in this function.

    • containingScope

      Scope containingScope()
      Returns:
      The scope containing this function.

    • statements

      Set<Statement> statements()
      Returns:
      The set of statements in this function.

    • startLocation

      Location startLocation()
      Returns:
      The first location in this function.

    • locations

      Set<Location> locations()
      Returns:
      The set of locations in this function.

    • model

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

    • setStatements

      void setStatements(Set<Statement> statements)
      Parameters:
      statements - The set of statements in this function.

    • setStartLocation

      void setStartLocation(Location startLocation)
      Parameters:
      startLocation - The first location in this function.

    • setLocations

      void setLocations(Set<Location> locations)
      Parameters:
      locations - The set of locations in this function.

    • addLocation

      void addLocation(Location location)
      Parameters:
      location - The new location to add.

    • addStatement

      void addStatement(Statement statement)
      Parameters:
      statement - The new statement to add.

    • setName

      void setName(Identifier name)
      Parameters:
      name - The name of this function.

    • setParameters

      void setParameters(List<Variable> parameters)
      Parameters:
      parameters - The list of parameters.

    • setScopes

      void setScopes(Set<Scope> scopes)
      Parameters:
      scopes - The set of scopes in this function.

    • setOuterScope

      void setOuterScope(Scope outerScope)
      Parameters:
      outerScope - The outermost local scope of this function.

    • setContainingScope

      void setContainingScope(Scope containingScope)
      Parameters:
      containingScope - The scope containing this function.

    • setModel

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

    • print

      void print(String prefix, PrintStream out, boolean isDebug)
      Print the function.
      Parameters:
      prefix - String prefix to print on each line
      out - The PrintStream to use for printing.
      isDebug - True iff the debugging option is enabled, when more information will be printed.

    • isRootFunction

      boolean isRootFunction()
      Returns:
      Is this the outermost function?

    • simplify

      void simplify()
      Remove all locations that satisfies the following conditions:
      1. has exactly one outgoing statement and
      2. the statement is a no-op with the guard being the true boolean expression.
      Meanwhile, have to redirect each statement that targets at the no-op location to the target of the no-op location. For example, let l(s->l', ...) be a location l with statement s going to l' ... l1 (s1 -> l2, s2 -> l3), l2 ([true]no-op -> l4), l3(), l(4) After applying simplify(), should be l1 (s1 -> l4, s2 -> l3), l3(), l4()

    • purelyLocalAnalysisForVariables

      void purelyLocalAnalysisForVariables()
      performs purely local analysis on variables for each statement/location of this function. No-op for system functions.

    • purelyLocalAnalysis

      void purelyLocalAnalysis()
      performs purely local analysis one each statement/location of this function, and concludes if the whole function is purely local or not.

    • variableAddressedOf

      Set<Variable> variableAddressedOf(Scope scope)
      returns the variables that are used as the operand of the address-of operator and are visible from the given lexical scope.
      Parameters:
      scope - a lexical scope
      Returns:
      returns the variables that are used as the operand of the address-of operator and are visible from the given lexical scope.

    • variableAddressedOf

      Set<Variable> variableAddressedOf()
      returns the variables that are used as the operand of the address-of operator.
      Returns:
      returns the variables that are used as the operand of the address-of operator and are visible from the given lexical scope.

    • functionType

      CIVLFunctionType functionType()
      returns the type of this function.
      Returns:
      the type of this function.

    • isSystemFunction

      boolean isSystemFunction()
      Is this a system function? A system function doesn't contain a function body and it is implemented by a library component in Java.
      Returns:
      true iff this function is a system function.

    • isAtomicFunction

      boolean isAtomicFunction()
      Is this an atomic function? An atomic function is declared with the specifier $atomic_f. Note that abstract functions and system functions are all atomic although they don't have the $atomic_f specifier.
      Returns:

    • isAbstractFunction

      boolean isAbstractFunction()
      Is this an abstract function?
      Returns:
      true iff this function is an abstract function.

    • isNormalFunction

      boolean isNormalFunction()
      Is this a normal function that contains a function body defined in the source code?
      Returns:
      true iff this is a normal function that contains a function body defined in the source code.

    • setReturnType

      void setReturnType(CIVLType returnType)
      updates the return type of this function
      Parameters:
      returnType - the type to be used as the return type of this function

    • setParameterTypes

      void setParameterTypes(CIVLType[] types)
      updates the types of the parameters of this function
      Parameters:
      types - the types to be used as the parameter types

    • unreachedCode

      StringBuffer unreachedCode()
      returns the string representation of all un-reached code (if any) in this function.
      Returns:
      the string representation of all un-reached code (if any) in this function

    • isPureFunction

      boolean isPureFunction()
      is this a pure function? i.e., a function that doesn't has side effect in the state
      Returns:

    • addPossibleValidConsequence

      void addPossibleValidConsequence(Pair<Expression,Integer> validConsequences)
      Possible valid consequence is a valid contract expression which is POSSIBLE a consequence of the whole contract Notice that consequences only come from requirements
      Parameters:
      validConsequences -

    • getPossibleValidConsequences

      List<Pair<Expression,Integer>> getPossibleValidConsequences()
      Possible valid consequence is a valid contract expression which is POSSIBLE a consequence of the whole contract Notice that consequences only come from requirements
      Parameters:
      validConsequences -

    • isContracted

      boolean isContracted()
      returns true if and only if the function is contracted.
      Returns:

    • functionContract

      FunctionContract functionContract()
      returns the contract specification of this function.
      Returns:

    • setFunctionContract

      void setFunctionContract(FunctionContract contract)
      sets the contract of this function.
      Parameters:
      contract -

    • computePathconditionOfLocations

      void computePathconditionOfLocations(ModelFactory modelFactory)

    • dependsNoact

      boolean dependsNoact()

    • isPurelyLocal

      boolean isPurelyLocal()
      is this function a purely local function?
      Returns:

    • setStateFunction

      void setStateFunction(boolean value)
      updates the property of this function to be a state function
      Parameters:
      value -

    • setPureFunction

      void setPureFunction(Boolean value)
      updates the property of this function to be pure
      Parameters:
      value -

    • isStateFunction

      boolean isStateFunction()
      returns true iff this function is a state function
      Returns:
      true iff this function is a state function

    • setFreeOfUnsafeloop

      void setFreeOfUnsafeloop(boolean noUnsafeloop)
      Parameters:
      noUnsafeloop - Set to true iff there is no unsafe loops in the LEXICAL function body. Unsafe loop is a loop whose start location doesn't satisfy that Location.isSafeLoop() returns true.

    • isFreeOfUnsafeloop

      boolean isFreeOfUnsafeloop()
      Returns:
      true iff there is no unsafe loops in the LEXICAL function body. Unsafe loop is a loop whose start location doesn't satisfy that Location.isSafeLoop() returns true.

    • isLogic

      boolean isLogic()
      Returns:
      true iff this function is a logic function. A call to a logic function is side-effect free.

    • setLogic

      void setLogic(boolean value)
      Set weather this function is a logic function.
      Parameters:
      value - true, to set the function as a logic function; false, otherwise.

    • setAccessesAtomicFunction

      void setAccessesAtomicFunction(Set<Variable> set)

    • getAccessesAtomicFunction

      Set<Variable> getAccessesAtomicFunction()