goto_functions.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Goto Programs with Functions
 
Author: Daniel Kroening
 
Date: June 2003
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H
#define CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H
 
#include "goto_function.h"
 
#include <util/cprover_prefix.h>
 
#include <map>
 
class goto_functionst
{
public:
  using goto_functiont=::goto_functiont;
  typedef std::map<irep_idt, goto_functiont> function_mapt;
  function_mapt function_map;
 
private:
  unsigned unused_location_number;
 
public:
  goto_functionst():
    unused_location_number(0)
  {
  }
 
  // Copying is unavailable as base class copy is deleted
  // MSVC is unable to automatically determine this
  goto_functionst(const goto_functionst &)=delete;
  goto_functionst &operator=(const goto_functionst &)=delete;
 
  // Move operations need to be explicitly enabled as they are deleted with the
  // copy operations
  // default for move operations isn't available on Windows yet, so define
  //  explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
  //  under "Defaulted and Deleted Functions")
 
  goto_functionst(goto_functionst &&other):
    function_map(std::move(other.function_map)),
    unused_location_number(other.unused_location_number)
  {
  }
 
  goto_functionst &operator=(goto_functionst &&other)
  {
    function_map=std::move(other.function_map);
    unused_location_number=other.unused_location_number;
    return *this;
  }
 
  void unload(const irep_idt &name) { function_map.erase(name); }
 
  void clear()
  {
    function_map.clear();
  }
 
  void compute_location_numbers();
  void compute_location_numbers(goto_programt &);
  void compute_loop_numbers();
  void compute_target_numbers();
  void compute_incoming_edges();
 
  void update()
  {
    compute_incoming_edges();
    compute_target_numbers();
    compute_location_numbers();
    compute_loop_numbers();
  }
 
  static inline irep_idt entry_point()
  {
    // do not confuse with C's "int main()"
    return CPROVER_PREFIX "_start";
  }
 
  void swap(goto_functionst &other)
  {
    function_map.swap(other.function_map);
  }
 
  void copy_from(const goto_functionst &other)
  {
    for(const auto &fun : other.function_map)
      function_map[fun.first].copy_from(fun.second);
  }
 
  std::vector<function_mapt::const_iterator> sorted() const;
  std::vector<function_mapt::iterator> sorted();
 
  void validate(const namespacet &, validation_modet) const;
};
 
#endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H