12#ifndef CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_ONLY_CHECKER_H
13#define CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_ONLY_CHECKER_H
Abstract interface to eager or lazy GOTO models.
ui_message_handlert & ui_message_handler
java_multi_path_symex_only_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
multi_path_symex_only_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
abstract_goto_modelt & goto_model
void java_setup_symex(const optionst &options, abstract_goto_modelt &goto_model, symex_bmct &symex)
Registers Java-specific preprocessing handlers with goto-symex.
Bounded Model Checking Utils for Java.
Goto Checker using Multi-Path Symbolic Execution only (no SAT solving)