java_trace_validation.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Java trace validation
 
Author: Jeannie Moulton
 
\*******************************************************************/
 
#ifndef CPROVER_JAVA_BYTECODE_JAVA_TRACE_VALIDATION_H
#define CPROVER_JAVA_BYTECODE_JAVA_TRACE_VALIDATION_H
 
#include <util/optional.h>
#include <util/validation_mode.h>
 
class goto_tracet;
class namespacet;
class exprt;
class address_of_exprt;
class constant_exprt;
class struct_exprt;
class symbol_exprt;
class member_exprt;
class messaget;
 
// clang-format off
#define OPT_JAVA_TRACE_VALIDATION /*NOLINT*/ \
  "(validate-trace)" \
 
#define HELP_JAVA_TRACE_VALIDATION /*NOLINT*/ \
    " --validate-trace             throw an error if the structure of the counterexample\n" /*NOLINT*/ \
    "                              trace does not match certain assumptions\n" /*NOLINT*/ \
    "                              (experimental, currently java only)\n" /*NOLINT*/ \
// clang-format on
 
void check_trace_assumptions(
  const goto_tracet &trace,
  const namespacet &ns,
  const messaget &log,
  const bool run_check = false,
  const validation_modet vm = validation_modet::INVARIANT);
 
bool check_symbol_structure(const exprt &expr);
 
optionalt<symbol_exprt> get_inner_symbol_expr(exprt expr);
 
bool check_member_structure(const member_exprt &expr);
 
bool valid_lhs_expr_high_level(const exprt &lhs);
 
bool valid_rhs_expr_high_level(const exprt &rhs);
 
bool can_evaluate_to_constant(const exprt &expression);
 
bool check_index_structure(const exprt &index_expr);
 
bool check_struct_structure(const struct_exprt &expr);
 
bool check_address_structure(const address_of_exprt &address);
 
bool check_constant_structure(const constant_exprt &constant_expr);
 
#endif // CPROVER_JAVA_BYTECODE_JAVA_TRACE_VALIDATION_H