CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
java_trace_validation.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Java trace validation
4
5Author: Jeannie Moulton
6
7\*******************************************************************/
8
9#ifndef CPROVER_JAVA_BYTECODE_JAVA_TRACE_VALIDATION_H
10#define CPROVER_JAVA_BYTECODE_JAVA_TRACE_VALIDATION_H
11
13
14#include <optional>
15
16class goto_tracet;
17class namespacet;
18class exprt;
20class constant_exprt;
21class struct_exprt;
22class symbol_exprt;
23class member_exprt;
24class messaget;
25
26// clang-format off
27#define OPT_JAVA_TRACE_VALIDATION /*NOLINT*/ \
28 "(validate-trace)" \
29
30#define HELP_JAVA_TRACE_VALIDATION /*NOLINT*/ \
31 " {y--validate-trace} \t throw an error if the structure of the" \
32 " counterexample trace does not match certain assumptions (experimental," \
33 " currently java only)\n"
34// clang-format on
35
41 const goto_tracet &trace,
42 const namespacet &ns,
43 const messaget &log,
44 const bool run_check = false,
46
49bool check_symbol_structure(const exprt &expr);
50
53std::optional<symbol_exprt> get_inner_symbol_expr(exprt expr);
54
57bool check_member_structure(const member_exprt &expr);
58
61bool valid_lhs_expr_high_level(const exprt &lhs);
62
65bool valid_rhs_expr_high_level(const exprt &rhs);
66
69bool can_evaluate_to_constant(const exprt &expression);
70
74
76bool check_struct_structure(const struct_exprt &expr);
77
79bool check_address_structure(const address_of_exprt &address);
80
83
84#endif // CPROVER_JAVA_BYTECODE_JAVA_TRACE_VALIDATION_H
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A constant literal expression.
Definition std_expr.h:3117
Base class for all expressions.
Definition expr.h:56
Trace of a GOTO program.
Definition goto_trace.h:177
Extract member of struct or union.
Definition std_expr.h:2971
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Struct constructor from list of elements.
Definition std_expr.h:1877
Expression to hold a symbol (variable)
Definition std_expr.h:131
bool valid_lhs_expr_high_level(const exprt &lhs)
std::optional< symbol_exprt > get_inner_symbol_expr(exprt expr)
Recursively extracts the first operand of an expression until it reaches a symbol and returns it,...
bool check_address_structure(const address_of_exprt &address)
bool valid_rhs_expr_high_level(const exprt &rhs)
bool check_member_structure(const member_exprt &expr)
bool check_index_structure(const exprt &index_expr)
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)
Checks that the structure of each step of the trace matches certain criteria.
bool check_symbol_structure(const exprt &expr)
bool check_constant_structure(const constant_exprt &constant_expr)
bool can_evaluate_to_constant(const exprt &expression)
bool check_struct_structure(const struct_exprt &expr)
double log(double x)
Definition math.c:2449
validation_modet