Module dev.civl.abc
Package dev.civl.abc.ast.entity.IF

Interface Function

All Superinterfaces:
Entity, OrdinaryEntity, ProgramEntity
public interface Function extends OrdinaryEntity
A function is an entity which takes inputs, executes a statement, and possibly returns a result.

  • Method Details

    • getType

      FunctionType getType()
      Description copied from interface: ProgramEntity

      Other than Label, and PragmaHandler, every kind of Entity has a type, returned by this method. For a Label or PragmaHandler, this returns null.

      The type is initially null. It can be set using method ProgramEntity.setType(Type).

      Specified by:
      getType in interface ProgramEntity
      Returns:
      the type of this entity or null

    • isInlined

      boolean isInlined()
      Is the function declared with the inline specifier, indicating that this is an inline function?
      Returns:
      true iff the function is an inline function

    • setIsInlined

      void setIsInlined(boolean value)
      Sets whether this function is an inline function
      Parameters:
      value - true if inlined, false if not

    • isAtomic

      boolean isAtomic()
      Is the function declared with the $atomic_f specifier, indicating that this is an atomic function?
      Returns:
      true iff the function is an atomic function

    • setAtomic

      void setAtomic(boolean value)
      Sets whether this function is an atomic function
      Parameters:
      value - true if atomic, false if not

    • isStateFunction

      boolean isStateFunction()

    • setStateFunction

      void setStateFunction(boolean value)

    • isLogic

      boolean isLogic()
      Returns:
      true iff this function is a logic function. The definition of a logic function is optional but if it exists it must be a (return of a) side-effect free expression. A logic function can be recursively defined since a call to a logic function is side-effect free as well.

      A logic function currently can only be defined in ACSL annotations

    • 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.

    • isPure

      boolean isPure()
      Is the function declared with the $pure specifier, indicating that this is a pure function?
      Returns:
      true iff the function is a pure function

    • setPure

      void setPure(boolean value)
      Sets whether this function is a pure function
      Parameters:
      value - true if pure, false if not

    • isAbstract

      boolean isAbstract()
      Is the function declared with the $abstract specifier, indicating that this is an abstract function?
      Returns:
      true iff the function is an abstract function

    • setAbstract

      void setAbstract(boolean value)
      Sets whether this function is an abstract function
      Parameters:
      value - true if abstract, false if not

    • isSystemFunction

      boolean isSystemFunction()
      Is the function declared with the $system specifier, indicating that this is a system function?
      Returns:
      true iff the function is a system function

    • setSystemFunction

      void setSystemFunction(boolean value)
      Sets whether this function is a system function
      Parameters:
      value - true if this is a system function, false if not

    • systemLibrary

      String systemLibrary()
      gets the library of this system function; null if this is not a system function.
      Returns:

    • setSystemLibrary

      void setSystemLibrary(String library)
      sets the library of this system function;
      Parameters:
      library -

    • doesNotReturn

      boolean doesNotReturn()
      Is the function declared with the _Noreturn specifier, indicating that the function does not return.
      Returns:
      true iff the function is declared with _Noreturn

    • setDoesNotReturn

      void setDoesNotReturn(boolean value)
      Sets whether this function is declared with _Noreturn.
      Parameters:
      value - true if _Noreturn, false if not

    • getDefinition

      FunctionDefinitionNode getDefinition()
      Description copied from interface: ProgramEntity

      Gets the definition, i.e., the defining declaration of this entity. Every entity has at most one definition. The definition is a declaration of a special kind. For example, for an object (variable), a definition is the declaration that allocates storage for that object. For a function, a definition is the declaration the contains the function body.

      The definition is initially null, but can be set using method ProgramEntity.setDefinition(DeclarationNode).

      Specified by:
      getDefinition in interface ProgramEntity
      Returns:
      the definition of this entity or null

    • getScope

      Scope getScope()
      Returns the function scope associated to this function. This is the scope in which the ordinary labels are declared. It is the outermost scope of the function body.
      Returns:
      the function scope associated to this function

    • getCallers

      Set<Function> getCallers()
      Returns the set of functions that call this function either by name or through a pointer dereference (the latter is relation is safely overapproximated). Transitive calling relationships are not reflected in this set, i.e., if a calls b which calls c, then a is not in getCallers() of c (unless of course a directly calls c as well). The set is initially empty; a call to CallAnalyzer.analyze(dev.civl.abc.ast.IF.AST) will populate it.
      Returns:
      the set of functions that call this function

    • getCallees

      Set<Function> getCallees()
      Returns the set of functions called by this function either by name or through a pointer dereference (the latter is relation is safely overapproximated). Transitive calling relationships are not reflected in this set, i.e., if a calls b which calls c, then c is not in getCallees() of a (unless of course a directly calls c as well). The set is initially empty; a call to CallAnalyzer.analyze(dev.civl.abc.ast.IF.AST) will populate it.
      Returns:
      the set of functions called by this function

    • addContract

      void addContract(ContractNode contract)
      Add a ContractNode which represents a contract clause.
      Parameters:
      contract - A node representing a contract clause.

    • getContracts

      Iterable<ContractNode> getContracts()
      Returns a Iterator for a set of contract clauses.
      Returns: