CBMC
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 <util/irep.h>
16 
17 class goto_functionst;
18 class symbol_table_baset;
19 class goto_modelt;
20 class goto_model_functiont;
21 class message_handlert;
22 struct java_object_factory_parameterst;
23 
38 void convert_nondet(
39  goto_functionst &goto_functions,
40  symbol_table_baset &symbol_table,
41  message_handlert &message_handler,
42  const java_object_factory_parameterst &object_factory_parameters);
43 
44 void convert_nondet(
45  goto_modelt &,
46  message_handlert &,
47  const java_object_factory_parameterst &object_factory_parameters);
48 
63 void convert_nondet(
64  goto_model_functiont &function,
65  message_handlert &message_handler,
66  const java_object_factory_parameterst &object_factory_parameters,
67  const irep_idt &mode);
68 
69 #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:38
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:190
goto_modelt
Definition: goto_model.h:27
message_handlert
Definition: message.h:28
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.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:217
java_object_factory_parameterst
Definition: java_object_factory_parameters.h:16