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
;
21
class
goto_model_functiont
;
22
class
message_handlert
;
23
struct
object_factory_parameterst
;
24
32
void
convert_nondet
(
33
goto_functionst
&,
34
symbol_table_baset
&,
35
message_handlert
&,
36
const
object_factory_parameterst
&object_factory_parameters);
37
38
void
convert_nondet
(
39
goto_modelt
&,
40
message_handlert
&,
41
const
object_factory_parameterst
&object_factory_parameters);
42
49
void
convert_nondet
(
50
goto_model_functiont
&
function
,
51
message_handlert
&
message_handler
,
52
const
object_factory_parameterst
&object_factory_parameters,
53
const
irep_idt
&mode);
54
55
#endif // CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H
goto_modelt
Definition:
goto_model.h:24
message_handlert
Definition:
message.h:25
goto_functionst
Definition:
goto_functions.h:21
dstringt
Definition:
dstring.h:21
irep.h
symbol_table_baset
The symbol table base class interface.
Definition:
symbol_table_base.h:21
message_handler
goto_programt coverage_criteriont message_handlert & message_handler
Definition:
cover.cpp:66
object_factory_parameterst
Definition:
object_factory_parameters.h:22
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
Definition:
goto_model.h:147
convert_nondet
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. ...
Definition:
convert_java_nondet.cpp:157
jbmc
src
java_bytecode
convert_java_nondet.h
Generated by
1.8.14