cprover
Loading...
Searching...
No Matches
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
12#include <util/optional.h>
14
15class goto_tracet;
16class namespacet;
17class exprt;
19class constant_exprt;
20class struct_exprt;
21class symbol_exprt;
22class member_exprt;
23class messaget;
24
25// clang-format off
26#define OPT_JAVA_TRACE_VALIDATION /*NOLINT*/ \
27 "(validate-trace)" \
28
29#define HELP_JAVA_TRACE_VALIDATION /*NOLINT*/ \
30 " {y--validate-trace} \t throw an error if the structure of the" \
31 " counterexample trace does not match certain assumptions (experimental," \
32 " currently java only)\n"
33// clang-format on
34
40 const goto_tracet &trace,
41 const namespacet &ns,
42 const messaget &log,
43 const bool run_check = false,
45
48bool check_symbol_structure(const exprt &expr);
49
53
56bool check_member_structure(const member_exprt &expr);
57
60bool valid_lhs_expr_high_level(const exprt &lhs);
61
64bool valid_rhs_expr_high_level(const exprt &rhs);
65
68bool can_evaluate_to_constant(const exprt &expression);
69
73
75bool check_struct_structure(const struct_exprt &expr);
76
78bool check_address_structure(const address_of_exprt &address);
79
82
83#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:563
A constant literal expression.
Definition std_expr.h:2942
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:2794
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
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:1819
Expression to hold a symbol (variable)
Definition std_expr.h:113
bool valid_lhs_expr_high_level(const exprt &lhs)
bool check_address_structure(const address_of_exprt &address)
bool valid_rhs_expr_high_level(const exprt &rhs)
optionalt< 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_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)
validation_modet