java_object_factory.h

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
#define CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H
 
#include "nondet.h"
 
#include <goto-programs/allocate_objects.h>
 
#include <util/std_code.h>
 
class message_handlert;
class select_pointer_typet;
class symbol_table_baset;
struct java_object_factory_parameterst;
 
exprt object_factory(
  const typet &type,
  const irep_idt base_name,
  code_blockt &init_code,
  symbol_table_baset &symbol_table,
  java_object_factory_parameterst parameters,
  lifetimet lifetime,
  const source_locationt &location,
  const select_pointer_typet &pointer_type_selector,
  message_handlert &log);
 
exprt object_factory(
  const typet &type,
  const irep_idt base_name,
  code_blockt &init_code,
  symbol_table_baset &symbol_table,
  const java_object_factory_parameterst &object_factory_parameters,
  lifetimet lifetime,
  const source_locationt &location,
  message_handlert &log);
 
enum class update_in_placet
{
  NO_UPDATE_IN_PLACE,
  MAY_UPDATE_IN_PLACE,
  MUST_UPDATE_IN_PLACE
};
 
void gen_nondet_init(
  const exprt &expr,
  code_blockt &init_code,
  symbol_table_baset &symbol_table,
  const source_locationt &loc,
  bool skip_classid,
  lifetimet lifetime,
  const java_object_factory_parameterst &object_factory_parameters,
  const select_pointer_typet &pointer_type_selector,
  update_in_placet update_in_place,
  message_handlert &log);
 
void gen_nondet_init(
  const exprt &expr,
  code_blockt &init_code,
  symbol_table_baset &symbol_table,
  const source_locationt &loc,
  bool skip_classid,
  lifetimet lifetime,
  const java_object_factory_parameterst &object_factory_parameters,
  update_in_placet update_in_place,
  message_handlert &log);
 
using array_element_generatort = std::function<
  code_blockt(const exprt &element_at_counter, const typet &element_type)>;
 
code_blockt gen_nondet_array_init(
  const exprt &expr,
  update_in_placet update_in_place,
  const source_locationt &location,
  const array_element_generatort &element_generator,
  const allocate_local_symbolt &allocate_local_symbol,
  const symbol_table_baset &symbol_table,
  size_t max_nondet_array_length);
 
#endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H