cbmc-documentation/java__object__factory_8h_source.html

/*******************************************************************\


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_tablet;

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_tablet &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_tablet &symbol_table,

  size_t max_nondet_array_length);


#endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H