CBMC
replace_java_nondet.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Replace Java Nondet expressions
4
5
Author: Reuben Thomas, reuben.thomas@diffblue.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_JAVA_BYTECODE_REPLACE_JAVA_NONDET_H
13
#define CPROVER_JAVA_BYTECODE_REPLACE_JAVA_NONDET_H
14
15
class
goto_modelt
;
16
class
goto_functionst
;
17
class
goto_model_functiont
;
18
19
void
replace_java_nondet
(
goto_modelt
&);
20
21
void
replace_java_nondet
(
goto_functionst
&);
22
23
void
replace_java_nondet
(
goto_model_functiont
&
function
);
24
25
#endif
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
replace_java_nondet
void replace_java_nondet(goto_modelt &)
Replace calls to nondet library functions with an internal nondet representation.
Definition:
replace_java_nondet.cpp:344
jbmc
src
java_bytecode
replace_java_nondet.h
Generated by
1.9.1