Loading...

Searching...

No Matches

java_bmc_util.h

1/*******************************************************************\

2

3Module: Bounded Model Checking Utils for Java

4

5Author: 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

16class optionst;

17class symex_bmct;

18

21 const optionst &options,

23 symex_bmct &symex);

24

25#endif // CPROVER_JAVA_BYTECODE_JAVA_BMC_UTIL_H

Abstract interface to eager or lazy GOTO models.

Definition abstract_goto_model.h:22

Definition options.h:23

Definition symex_bmc.h:24

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

CBMC: /home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_bmc_util.h Source File