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

Interface FunctionContract

All Superinterfaces:
Sourceable
public interface FunctionContract extends Sourceable
This represents a block of ACSL contract for a function.

  • Method Details

    • defaultBehavior

      FunctionBehavior defaultBehavior()
      Returns the default behavior of the function.
      Returns:

    • namedBehaviors

      Iterable<NamedFunctionBehavior> namedBehaviors()
      Returns the named behaviors of the function.
      Returns:

    • guard

      Expression guard()
      Returns the guard of the function.
      Returns:

    • isPure

      boolean isPure()
      Does the contract contains pure clause?
      Returns:

    • setPure

      void setPure(boolean value)
      Updates the contract to denote if it contains pure clause.
      Parameters:
      value -

    • setGuard

      void setGuard(Expression expression)
      Sets the guard of the function.
      Parameters:
      expression -

    • setDefaultBehavior

      void setDefaultBehavior(FunctionBehavior behavior)
      Sets the default behavior of the function.
      Parameters:
      behavior -

    • addNamedBehavior

      void addNamedBehavior(NamedFunctionBehavior behavior)
      Adds a named behavior to the function.
      Parameters:
      behavior -

    • getBehavior

      NamedFunctionBehavior getBehavior(String name)
      returns the behavior with the given name; null if no such behavior exists.
      Parameters:
      name -
      Returns:

    • print

      void print(String prefix, PrintStream out, boolean isDebug)
      prints this function contract
      Parameters:
      prefix -
      out -
      isDebug -

    • hasReadsClause

      boolean hasReadsClause()
      is there reads clause in this contract?
      Returns:

    • hasAssignsClause

      boolean hasAssignsClause()
      is there assigns clause in this contract?
      Returns:

    • hasDependsClause

      boolean hasDependsClause()
      is there depends clause in this contract?
      Returns:

    • hasRequirementsOrEnsurances

      boolean hasRequirementsOrEnsurances()
      is there any requirements or ensurances ?
      Returns:

    • scope

      Scope scope()
      The static scope in which the function contract exists. Not necessarily the same as the function definition's parameter scope, because the contract may have been associated with a function prototype.
      Returns:
      scope in which contract exists