allocate_objects.h

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
#ifndef CPROVER_UTIL_ALLOCATE_OBJECTS_H
#define CPROVER_UTIL_ALLOCATE_OBJECTS_H
 
#include <util/namespace.h>
#include <util/std_code.h>
 
enum class lifetimet
{
  AUTOMATIC_LOCAL,
  STATIC_GLOBAL,
  DYNAMIC
};
 
class allocate_objectst
{
public:
  allocate_objectst(
    const irep_idt &symbol_mode,
    const source_locationt &source_location,
    const irep_idt &name_prefix,
    symbol_table_baset &symbol_table)
    : symbol_mode(symbol_mode),
      source_location(source_location),
      name_prefix(name_prefix),
      symbol_table(symbol_table),
      ns(symbol_table)
  {
  }
 
  exprt allocate_object(
    code_blockt &assignments,
    const exprt &target_expr,
    const typet &allocate_type,
    const lifetimet lifetime,
    const irep_idt &basename_prefix = "tmp");
 
  exprt allocate_automatic_local_object(
    code_blockt &assignments,
    const exprt &target_expr,
    const typet &allocate_type,
    const irep_idt &basename_prefix = "tmp");
 
  exprt allocate_static_global_object(
    code_blockt &assignments,
    const exprt &target_expr,
    const typet &allocate_type,
    const irep_idt &basename_prefix = "tmp");
 
  exprt allocate_dynamic_object_symbol(
    code_blockt &output_code,
    const exprt &target_expr,
    const typet &allocate_type);
 
  exprt allocate_dynamic_object(
    code_blockt &output_code,
    const exprt &target_expr,
    const typet &allocate_type);
 
  symbol_exprt allocate_automatic_local_object(
    const typet &allocate_type,
    const irep_idt &basename_prefix = "tmp");
 
  void add_created_symbol(const symbolt &symbol);
 
  void declare_created_symbols(code_blockt &init_code);
 
  void mark_created_symbols_as_input(code_blockt &init_code);
 
private:
  const irep_idt symbol_mode;
  const source_locationt source_location;
  const irep_idt name_prefix;
 
  symbol_table_baset &symbol_table;
  const namespacet ns;
 
  std::vector<irep_idt> symbols_created;
 
  exprt allocate_non_dynamic_object(
    code_blockt &assignments,
    const exprt &target_expr,
    const typet &allocate_type,
    const bool static_lifetime,
    const irep_idt &basename_prefix);
};
 
code_frontend_assignt
make_allocate_code(const symbol_exprt &lhs, const exprt &size);
 
#endif // CPROVER_UTIL_ALLOCATE_OBJECTS_H