cprover
java_single_path_symex_checker.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Checker using Single Path Symbolic Execution for Java
4 
5 Author: Jeannie Moulton
6 
7  \*******************************************************************/
8 
10 #include "java_trace_validation.h"
11 
13 {
16  goto_trace, ns, log, options.get_bool_option("validate-trace"));
17  return goto_trace;
18 }
19 
21 {
24  goto_trace, ns, log, options.get_bool_option("validate-trace"));
25  return goto_trace;
26 }
27 
30 {
31  goto_tracet goto_trace = single_path_symex_checkert::build_trace(property_id);
33  goto_trace, ns, log, options.get_bool_option("validate-trace"));
34  return goto_trace;
35 }
single_path_symex_checkert::build_trace
goto_tracet build_trace(const irep_idt &) const override
Builds and returns the trace for the FAILed property with the given property_id.
Definition: single_path_symex_checker.cpp:153
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
single_path_symex_only_checkert::ns
namespacet ns
Definition: single_path_symex_only_checker.h:37
check_trace_assumptions
void check_trace_assumptions(const goto_tracet &trace, const namespacet &ns, const messaget &log, const bool run_check, const validation_modet vm)
Checks that the structure of each step of the trace matches certain criteria.
Definition: java_trace_validation.cpp:302
incremental_goto_checkert::options
const optionst & options
Definition: incremental_goto_checker.h:89
java_trace_validation.h
incremental_goto_checkert::log
messaget log
Definition: incremental_goto_checker.h:91
java_single_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_single_path_symex_checker.cpp:29
single_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: single_path_symex_checker.cpp:132
java_single_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_single_path_symex_checker.cpp:20
java_single_path_symex_checker.h
Goto Checker using Single Path Symbolic Execution for Java.
single_path_symex_checkert::build_full_trace
goto_tracet build_full_trace() const override
Builds and returns the complete trace.
Definition: single_path_symex_checker.cpp:119
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:171
java_single_path_symex_checkert::build_full_trace
goto_tracet build_full_trace() const override
Builds and returns the complete trace.
Definition: java_single_path_symex_checker.cpp:12