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/validation_mode.h>
 
#include <optional>
 
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*/ \
  " {y--validate-trace} \t throw an error if the structure of the" \
  " counterexample trace does not match certain assumptions (experimental," \
  " currently java only)\n"
// 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);

std::optional<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