cprover
convert_java_nondet.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Convert side_effect_expr_nondett expressions
4 
5 Author: Reuben Thomas, reuben.thomas@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H
13 #define CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H
14 
15 #include <cstddef> // size_t
16 #include <util/irep.h>
17 
18 class goto_functionst;
19 class symbol_table_baset;
20 class goto_modelt;
22 class message_handlert;
24 
39 void convert_nondet(
40  goto_functionst &goto_functions,
41  symbol_table_baset &symbol_table,
42  message_handlert &message_handler,
43  const java_object_factory_parameterst &object_factory_parameters);
44 
45 void convert_nondet(
46  goto_modelt &,
48  const java_object_factory_parameterst &object_factory_parameters);
49 
64 void convert_nondet(
65  goto_model_functiont &function,
66  message_handlert &message_handler,
67  const java_object_factory_parameterst &object_factory_parameters,
68  const irep_idt &mode);
69 
70 #endif // CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_modelt
Definition: goto_model.h:26
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
message_handlert
Definition: message.h:28
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
convert_nondet
void convert_nondet(goto_functionst &goto_functions, symbol_table_baset &symbol_table, message_handlert &message_handler, const java_object_factory_parameterst &object_factory_parameters)
Converts side_effect_exprt_nondett expressions using java_object_factory.
Definition: convert_java_nondet.cpp:219
java_object_factory_parameterst
Definition: java_object_factory_parameters.h:16
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
irep.h