CBMC
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 
9 #include "java_multi_path_symex_checker.h"
10 #include "java_trace_validation.h"
11 
12 goto_tracet java_multi_path_symex_checkert::build_full_trace() const
13 {
14  goto_tracet goto_trace = multi_path_symex_checkert::build_full_trace();
15  check_trace_assumptions(
16  goto_trace, ns, log, options.get_bool_option("validate-trace"));
17  return goto_trace;
18 }
19 
20 goto_tracet
21 java_multi_path_symex_checkert::build_trace(const irep_idt &property_id) const
22 {
23  goto_tracet goto_trace = multi_path_symex_checkert::build_trace(property_id);
24  check_trace_assumptions(
25  goto_trace, ns, log, options.get_bool_option("validate-trace"));
26  return goto_trace;
27 }
28 
29 goto_tracet java_multi_path_symex_checkert::build_shortest_trace() const
30 {
31  goto_tracet goto_trace = multi_path_symex_checkert::build_shortest_trace();
32  check_trace_assumptions(
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:38
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:177
incremental_goto_checkert::log
messaget log
Definition: incremental_goto_checker.h:93
incremental_goto_checkert::options
const optionst & options
Definition: incremental_goto_checker.h:91
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::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::build_full_trace
goto_tracet build_full_trace() const override
Builds and returns the complete trace.
Definition: multi_path_symex_checker.cpp:97
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:110
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:127
multi_path_symex_only_checkert::ns
namespacet ns
Definition: multi_path_symex_only_checker.h:36
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
java_multi_path_symex_checker.h
Goto Checker using Bounded Model Checking for Java.
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:314
java_trace_validation.h