cprover
java_single_path_symex_only_checker.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Checker using Single Path Symbolic Execution for Java
4 
5 Author: 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 {
22 public:
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
java_single_path_symex_only_checkert
Definition: java_single_path_symex_only_checker.h:21
java_bmc_util.h
Bounded Model Checking Utils for Java.
single_path_symex_only_checkert::setup_symex
virtual void setup_symex(symex_bmct &symex)
Definition: single_path_symex_only_checker.cpp:139
ui_message_handlert
Definition: ui_message.h:20
optionst
Definition: options.h:23
incremental_goto_checkert::options
const optionst & options
Definition: incremental_goto_checker.h:89
single_path_symex_only_checkert::goto_model
abstract_goto_modelt & goto_model
Definition: single_path_symex_only_checker.h:35
java_single_path_symex_only_checkert::setup_symex
void setup_symex(symex_bmct &symex) override
Definition: java_single_path_symex_only_checker.h:31
single_path_symex_only_checkert
Uses goto-symex to generate a symex_target_equationt for each path.
Definition: single_path_symex_only_checker.h:23
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:21
java_single_path_symex_only_checkert::java_single_path_symex_only_checkert
java_single_path_symex_only_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
Definition: java_single_path_symex_only_checker.h:23
symex_bmct
Definition: symex_bmc.h:26
incremental_goto_checkert::ui_message_handler
ui_message_handlert & ui_message_handler
Definition: incremental_goto_checker.h:90
single_path_symex_only_checker.h
Goto Checker using Single Path Symbolic Execution only.
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