CBMC
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 
9 #include "java_single_path_symex_checker.h"
10 #include "java_trace_validation.h"
11 
12 goto_tracet java_single_path_symex_checkert::build_full_trace() const
13 {
14  goto_tracet goto_trace = single_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 java_single_path_symex_checkert::build_shortest_trace() const
21 {
22  goto_tracet goto_trace = single_path_symex_checkert::build_shortest_trace();
23  check_trace_assumptions(
24  goto_trace, ns, log, options.get_bool_option("validate-trace"));
25  return goto_trace;
26 }
27 
28 goto_tracet
29 java_single_path_symex_checkert::build_trace(const irep_idt &property_id) const
30 {
31  goto_tracet goto_trace = single_path_symex_checkert::build_trace(property_id);
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_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
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
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
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
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:162
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:128
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:141
single_path_symex_only_checkert::ns
namespacet ns
Definition: single_path_symex_only_checker.h:40
java_single_path_symex_checker.h
Goto Checker using Single Path Symbolic Execution 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