convert_java_nondet.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Convert side_effect_expr_nondett expressions
 
Author: Reuben Thomas, reuben.thomas@diffblue.com
 
\*******************************************************************/

 
#ifndef CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H
#define CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H
 
#include <util/irep.h>
 
class goto_functionst;
class symbol_table_baset;
class goto_modelt;
class goto_model_functiont;
class message_handlert;
struct java_object_factory_parameterst;

void convert_nondet(
  goto_functionst &goto_functions,
  symbol_table_baset &symbol_table,
  message_handlert &message_handler,
  const java_object_factory_parameterst &object_factory_parameters);
 
void convert_nondet(
  goto_modelt &,
  message_handlert &,
  const java_object_factory_parameterst &object_factory_parameters);

void convert_nondet(
  goto_model_functiont &function,
  message_handlert &message_handler,
  const java_object_factory_parameterst &object_factory_parameters,
  const irep_idt &mode);
 
#endif // CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H