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 
12 #include <solvers/prop/prop.h>
13 
15 {
18  goto_trace, ns, log, options.get_bool_option("validate-trace"));
19  return goto_trace;
20 }
21 
24 {
25  goto_tracet goto_trace = multi_path_symex_checkert::build_trace(property_id);
27  goto_trace, ns, log, options.get_bool_option("validate-trace"));
28  return goto_trace;
29 }
30 
32 {
35  goto_trace, ns, log, options.get_bool_option("validate-trace"));
36  return goto_trace;
37 }
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:175
goto_tracet build_shortest_trace() const override
Builds and returns the trace up to the first failed property.
goto_tracet build_full_trace() const override
Builds and returns the complete 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.
goto_tracet build_full_trace() const override
Builds and returns the complete trace.
goto_tracet build_shortest_trace() const override
Builds and returns the trace up to the first failed property.
goto_tracet build_trace(const irep_idt &) const override
Builds and returns the trace for the FAILed property with the given property_id.
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
Goto Checker using Bounded Model Checking for Java.
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.