cprover
java_single_path_symex_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_CHECKER_H
13 #define CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_CHECKER_H
14 
15 #include <goto-checker/bmc_util.h>
19 
20 #include "java_bmc_util.h"
21 #include "java_trace_validation.h"
22 
24 {
25 public:
27  const optionst &options,
31  {
32  }
33 
34  void setup_symex(symex_bmct &symex) override
35  {
38  }
39 
40  goto_tracet build_full_trace() const override;
41  goto_tracet build_shortest_trace() const override;
42  goto_tracet build_trace(const irep_idt &property_id) const override;
43 };
44 
45 #endif // CPROVER_JAVA_BYTECODE_JAVA_SINGLE_PATH_SYMEX_CHECKER_H
Bounded Model Checking Utilities.
Traces of GOTO Programs.
Abstract interface to eager or lazy GOTO models.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Trace of a GOTO program.
Definition: goto_trace.h:177
ui_message_handlert & ui_message_handler
void setup_symex(symex_bmct &symex) override
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.
goto_tracet build_full_trace() const override
Builds and returns the complete trace.
java_single_path_symex_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
goto_tracet build_shortest_trace() const override
Builds and returns the trace up to the first failed property.
Uses goto-symex to symbolically execute each path in the goto model and calls a solver to find proper...
virtual void setup_symex(symex_bmct &symex)
Counterexample Beautification.
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.