cbmc/java__single__path__symex__checker_8cpp_source.html

/*******************************************************************\


Module: Goto Checker using Single Path Symbolic Execution for Java


Author: Jeannie Moulton


\*******************************************************************/


#include "java_single_path_symex_checker.h"

#include "java_trace_validation.h"


goto_tracet java_single_path_symex_checkert::build_full_trace() const

{

  goto_tracet goto_trace = single_path_symex_checkert::build_full_trace();

  check_trace_assumptions(

    goto_trace, ns, log, options.get_bool_option("validate-trace"));

  return goto_trace;

}

goto_tracet java_single_path_symex_checkert::build_full_trace() const {…}


goto_tracet java_single_path_symex_checkert::build_shortest_trace() const

{

  goto_tracet goto_trace = single_path_symex_checkert::build_shortest_trace();

  check_trace_assumptions(

    goto_trace, ns, log, options.get_bool_option("validate-trace"));

  return goto_trace;

}

goto_tracet java_single_path_symex_checkert::build_shortest_trace() const {…}


goto_tracet


java_single_path_symex_checkert::build_trace(const irep_idt &property_id) const

{

  goto_tracet goto_trace = single_path_symex_checkert::build_trace(property_id);

  check_trace_assumptions(

    goto_trace, ns, log, options.get_bool_option("validate-trace"));

  return goto_trace;

}

java_single_path_symex_checkert::build_trace(const irep_idt &property_id) const {…}

ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562

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

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