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 
32 void convert_nondet(
36  const object_factory_parameterst &object_factory_parameters);
37 
38 void convert_nondet(
39  goto_modelt &,
41  const object_factory_parameterst &object_factory_parameters);
42 
49 void convert_nondet(
50  goto_model_functiont &function,
52  const object_factory_parameterst &object_factory_parameters,
53  const irep_idt &mode);
54 
55 #endif // CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
The symbol table base class interface.
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
Definition: goto_model.h:147
void convert_nondet(goto_functionst &, symbol_table_baset &, message_handlert &, const object_factory_parameterst &object_factory_parameters)
Replace calls to nondet library functions with an internal nondet representation. ...