cprover
Loading...
Searching...
No Matches
java_single_path_symex_only_checker.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Checker using Single Path Symbolic Execution for Java
4
5Author: Daniel Kroening, Peter Schrammel
6
7 \*******************************************************************/
8
11
12#ifndef CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_ONLY_CHECKER_H
13#define CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_ONLY_CHECKER_H
14
16
17#include "java_bmc_util.h"
18
21{
22public:
24 const optionst &options,
28 {
29 }
30
31 void setup_symex(symex_bmct &symex) override
32 {
35 }
36};
37
38#endif // CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_ONLY_CHECKER_H
Abstract interface to eager or lazy GOTO models.
ui_message_handlert & ui_message_handler
java_single_path_symex_only_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
Uses goto-symex to generate a symex_target_equationt for each path.
virtual void setup_symex(symex_bmct &symex)
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 Single Path Symbolic Execution only.