Loading...

Searching...

No Matches

Macros | Functions

java_trace_validation.h File Reference

#include <util/validation_mode.h>
#include <optional>

+ Include dependency graph for java_trace_validation.h:

[フレーム]

+ This graph shows which files directly or indirectly include this file:

[フレーム]

Go to the source code of this file.

Macros

#define OPT_JAVA_TRACE_VALIDATION

#define HELP_JAVA_TRACE_VALIDATION

Functions

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)

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, or returns an empty optional.

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)

Macro Definition Documentation

◆ HELP_JAVA_TRACE_VALIDATION

#define HELP_JAVA_TRACE_VALIDATION

Value:

/*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"

Definition at line 30 of file java_trace_validation.h.

◆ OPT_JAVA_TRACE_VALIDATION

#define OPT_JAVA_TRACE_VALIDATION

Value:

/*NOLINT*/ \

"(validate-trace)" \

Definition at line 27 of file java_trace_validation.h.

Function Documentation

◆ can_evaluate_to_constant()

bool can_evaluate_to_constant ( const exprt & expression )

Returns: true iff the expression is a constant or symbol expression, i.e., one that can be evaluated to a literal, as for for a index value

Definition at line 78 of file java_trace_validation.cpp.

◆ check_address_structure()

bool check_address_structure ( const address_of_exprt & address )

Returns: true iff the address_of_exprt has a valid symbol operand

Definition at line 118 of file java_trace_validation.cpp.

◆ check_constant_structure()

bool check_constant_structure ( const constant_exprt & constant_expr )

Returns: true iff the constant_exprt has valid operands and value

Definition at line 124 of file java_trace_validation.cpp.

◆ check_index_structure()

bool check_index_structure ( const exprt & index_expr )

Returns: true iff the expression is an index expression and has a valid symbol and index value as operands

Definition at line 86 of file java_trace_validation.cpp.

◆ check_member_structure()

bool check_member_structure ( const member_exprt & expr )

Returns: true iff the expression is a member expression (or nested member expression) of a valid symbol

Definition at line 52 of file java_trace_validation.cpp.

◆ check_struct_structure()

bool check_struct_structure ( const struct_exprt & expr )

Returns: true iff the struct expression and has valid operands

Definition at line 95 of file java_trace_validation.cpp.

◆ check_symbol_structure()

bool check_symbol_structure ( const exprt & expr )

Returns: true iff the expression is a symbol expression and has a non-empty identifier

Definition at line 21 of file java_trace_validation.cpp.

◆ check_trace_assumptions()

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.

If it does not, throw an error. Intended to be called by the caller of build_goto_trace, for example java_multi_path_symex_checkert::build_full_trace()

Definition at line 314 of file java_trace_validation.cpp.

◆ get_inner_symbol_expr()

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, or returns an empty optional.

Definition at line 39 of file java_trace_validation.cpp.

◆ valid_lhs_expr_high_level()

bool valid_lhs_expr_high_level ( const exprt & lhs )

Returns: true iff the left hand side is superficially an expected expression type

Definition at line 60 of file java_trace_validation.cpp.

◆ valid_rhs_expr_high_level()

bool valid_rhs_expr_high_level ( const exprt & rhs )

Returns: true iff the right hand side is superficially an expected expression type

Definition at line 67 of file java_trace_validation.cpp.