cprover
java_single_path_symex_checker.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Checker using Single Path Symbolic Execution for Java
4
5Author: Jeannie Moulton
6
7 \*******************************************************************/
8
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
23{
26 goto_trace, ns, log, options.get_bool_option("validate-trace"));
27 return goto_trace;
28}
29
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_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.
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
goto_tracet build_trace(const irep_idt &) 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 Checker using Single Path Symbolic Execution 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.