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_modelt
Definition: goto_model.h:25
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:347
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:24
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:182