CBMC
java_bmc_util.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Bounded Model Checking Utils for Java
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BMC_UTIL_H
13 #define CPROVER_JAVA_BYTECODE_JAVA_BMC_UTIL_H
14 
15 class abstract_goto_modelt;
16 class optionst;
17 class symex_bmct;
18 
20 void java_setup_symex(
21  const optionst &options,
22  abstract_goto_modelt &goto_model,
23  symex_bmct &symex);
24 
25 #endif // CPROVER_JAVA_BYTECODE_JAVA_BMC_UTIL_H
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:22
symex_bmct
Definition: symex_bmc.h:24
java_setup_symex
void java_setup_symex(const optionst &options, abstract_goto_modelt &goto_model, symex_bmct &symex)
Registers Java-specific preprocessing handlers with goto-symex.
Definition: java_bmc_util.cpp:18