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

Interface Model

All Superinterfaces:
Sourceable
public interface Model extends Sourceable
A model of a CIVL program. This is the "low-level" intermediate representation of a CIVL program. It is the thing that is executed using model checking and/or symbolic execution techniques.

  • Method Details

    • staticConstantScope

      Scope staticConstantScope()
      returns the scope for constants
      Returns:

    • factory

      ModelFactory factory()
      Returns:
      The model factory that created this model.

    • setName

      void setName(String name)
      Parameters:
      name - The name of this model.

    • name

      String name()
      Returns:
      The name of this model.

    • functions

      Set<CIVLFunction> functions()
      Returns:
      The set of all functions in the model.

    • rootFunction

      CIVLFunction rootFunction()
      Returns:
      The root function which usually wraps the main function

    • setFunctions

      void setFunctions(Set<CIVLFunction> functions)
      Parameters:
      functions - The set of all functions in the model.

    • setRootFunction

      void setRootFunction(CIVLFunction root)
      Parameters:
      root - The root function which usually wraps the main function

    • addFunction

      void addFunction(CIVLFunction function)
      Parameters:
      function - The function to be added to the model.

    • function

      CIVLFunction function(String name)
      Get a function based on its name.
      Parameters:
      name - The name of the function.
      Returns:
      The function with the given name. Null if not found.

    • print

      void print(PrintStream out, boolean isDebug)
      Print the model.
      Parameters:
      out - The PrintStream used to print the model.
      isDebug - True iff the debugigng option is enabled, when more information will be printed, such as purely local marks, location loops, etc.

    • setExternVariables

      void setExternVariables(Map<String,Variable> externVariables)
      Parameters:
      externVariables - Map of names to variables for all extern variables used in this model.

    • externVariables

      Map<String,Variable> externVariables()
      Returns:
      Map of names to variables for all extern variables used in this model.

    • getNumMallocs

      int getNumMallocs()
      Returns:
      the number of malloc and malloc-equivalent (e.g., gcomm_create) statements in the model

    • getMalloc

      MallocStatement getMalloc(int index)
      Parameters:
      index - the index of the malloc statement
      Returns:
      the malloc statement of the given index

    • setQueueType

      void setQueueType(CIVLType queueType)
      Parameters:
      queueType - The queue type used by this model.

    • setMessageType

      void setMessageType(CIVLType messageType)
      Parameters:
      messageType - The message type used by this model.

    • queueType

      CIVLType queueType()
      Returns:
      The queue type used by this model.

    • mesageType

      CIVLType mesageType()
      Returns:
      The message type used by this model.

    • bundleType

      CIVLBundleType bundleType()
      Returns:
      The bundle type used by this model.

    • setBundleType

      void setBundleType(CIVLBundleType type)
      updates the bundle type of the model
      Parameters:
      type - the bundle type

    • complete

      void complete()
      Complete the model. This should be called as the last call for manipulating the model.

    • setHasFscanf

      void setHasFscanf(boolean value)
      updates the flag which denotes either the model contains any fscanf call or not.
      Parameters:
      value -

    • hasFscanf

      boolean hasFscanf()
      Returns:
      true iff the model contains any fscanf call

    • program

      dev.civl.abc.program.IF.Program program()
      Returns:
      the program object associates with this model

    • printUnreachedCode

      void printUnreachedCode(PrintStream out)
      prints the unreached code of the model
      Parameters:
      out - the output stream

    • outputVariables

      List<Variable> outputVariables()
      Return the output variables of this model, which all belong to the root scope.
      Returns:
      the output variables of this model, which all belong to the root scope

    • setSleepLocation

      void setSleepLocation(Location sleep)

    • sleepLocation

      Location sleepLocation()

    • hasStateRefVariables

      boolean hasStateRefVariables()
      does this model contain any variable that involves state references ($state type)?
      Returns:

    • getAllLogicFunctions

      List<LogicFunction> getAllLogicFunctions()
      Returns:
      All seen LogicFunctions that are with definitions.

    • setLogicFunctions

      void setLogicFunctions(List<LogicFunction> logicFunctions)
      Adding all translated logic functions to the model
      Parameters:
      logicFunctions - the translated logic functions that will be added to the model