cprover
java_trace_validation.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Java trace validation
4 
5 Author: 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>
13 #include <util/validation_mode.h>
14 
15 class goto_tracet;
16 class namespacet;
17 class exprt;
18 class address_of_exprt;
19 class constant_exprt;
20 class struct_exprt;
21 class symbol_exprt;
22 class member_exprt;
23 class 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  " --validate-trace throw an error if the structure of the counterexample\n" /*NOLINT*/ \
31  " trace does not match certain assumptions\n" /*NOLINT*/ \
32  " (experimental, currently java only)\n" /*NOLINT*/ \
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 
48 bool check_symbol_structure(const exprt &expr);
49 
53 
56 bool check_member_structure(const member_exprt &expr);
57 
60 bool valid_lhs_expr_high_level(const exprt &lhs);
61 
64 bool valid_rhs_expr_high_level(const exprt &rhs);
65 
68 bool can_evaluate_to_constant(const exprt &expression);
69 
72 bool check_index_structure(const exprt &index_expr);
73 
75 bool check_struct_structure(const struct_exprt &expr);
76 
78 bool check_address_structure(const address_of_exprt &address);
79 
81 bool check_constant_structure(const constant_exprt &constant_expr);
82 
83 #endif // CPROVER_JAVA_BYTECODE_JAVA_TRACE_VALIDATION_H
Operator to return the address of an object.
Definition: pointer_expr.h:200
A constant literal expression.
Definition: std_expr.h:2668
Base class for all expressions.
Definition: expr.h:54
Trace of a GOTO program.
Definition: goto_trace.h:177
Extract member of struct or union.
Definition: std_expr.h:2528
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:92
Struct constructor from list of elements.
Definition: std_expr.h:1583
Expression to hold a symbol (variable)
Definition: std_expr.h:81
bool valid_lhs_expr_high_level(const exprt &lhs)
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_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)
nonstd::optional< T > optionalt
Definition: optional.h:35
validation_modet