cprover
java_multi_path_symex_checker.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Checker using Bounded Model Checking 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 
22 {
23  goto_tracet goto_trace = multi_path_symex_checkert::build_trace(property_id);
25  goto_trace, ns, log, options.get_bool_option("validate-trace"));
26  return goto_trace;
27 }
28 
30 {
33  goto_trace, ns, log, options.get_bool_option("validate-trace"));
34  return goto_trace;
35 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.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
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: multi_path_symex_checker.cpp:102
incremental_goto_checkert::log
messaget log
Definition: incremental_goto_checker.h:91
multi_path_symex_only_checkert::ns
namespacet ns
Definition: multi_path_symex_only_checker.h:32
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
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
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
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
multi_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: multi_path_symex_checker.cpp:120
multi_path_symex_checkert::build_full_trace
goto_tracet build_full_trace() const override
Builds and returns the complete trace.
Definition: multi_path_symex_checker.cpp:89
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:171
java_multi_path_symex_checker.h
Goto Checker using Bounded Model Checking for Java.