CBMC
java_multi_path_symex_checker.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Checker using Bounded Model Checking for Java
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_CHECKER_H
13 #define CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_CHECKER_H
14 
15 #include <goto-checker/multi_path_symex_checker.h>
16 
17 #include "java_bmc_util.h"
18 
19 class java_multi_path_symex_checkert : public multi_path_symex_checkert
20 {
21 public:
22  java_multi_path_symex_checkert(
23  const optionst &options,
24  ui_message_handlert &ui_message_handler,
25  abstract_goto_modelt &goto_model)
26  : multi_path_symex_checkert(options, ui_message_handler, goto_model)
27  {
28  java_setup_symex(options, goto_model, symex);
29  }
30 
31  goto_tracet build_full_trace() const override;
32  goto_tracet build_trace(const irep_idt &property_id) const override;
33  goto_tracet build_shortest_trace() const override;
34 };
35 
36 #endif // CPROVER_JAVA_BYTECODE_JAVA_MULTI_PATH_SYMEX_CHECKER_H
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:22
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:177
incremental_goto_checkert::options
const optionst & options
Definition: incremental_goto_checker.h:91
incremental_goto_checkert::ui_message_handler
ui_message_handlert & ui_message_handler
Definition: incremental_goto_checker.h:92
java_multi_path_symex_checkert
Definition: java_multi_path_symex_checker.h:20
java_multi_path_symex_checkert::build_shortest_trace
goto_tracet build_shortest_trace() const override
Builds and returns the trace up to the first failed property.
Definition: java_multi_path_symex_checker.cpp:29
java_multi_path_symex_checkert::java_multi_path_symex_checkert
java_multi_path_symex_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
Definition: java_multi_path_symex_checker.h:22
java_multi_path_symex_checkert::build_full_trace
goto_tracet build_full_trace() const override
Builds and returns the complete trace.
Definition: java_multi_path_symex_checker.cpp:12
java_multi_path_symex_checkert::build_trace
goto_tracet build_trace(const irep_idt &property_id) const override
Builds and returns the trace for the FAILed property with the given property_id.
Definition: java_multi_path_symex_checker.cpp:21
multi_path_symex_checkert
Performs a multi-path symbolic execution using goto-symex and calls a SAT/SMT solver to check the sta...
Definition: multi_path_symex_checker.h:29
multi_path_symex_only_checkert::symex
symex_bmct symex
Definition: multi_path_symex_only_checker.h:41
multi_path_symex_only_checkert::goto_model
abstract_goto_modelt & goto_model
Definition: multi_path_symex_only_checker.h:34
ui_message_handlert
Definition: ui_message.h:22
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
java_bmc_util.h
Bounded Model Checking Utils for Java.
multi_path_symex_checker.h
Goto Checker using Multi-Path Symbolic Execution.