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

Include dependency graph for java_trace_validation.h:

This graph shows which files directly or indirectly include 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. More...

bool	check_symbol_structure (const exprt &expr)

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

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*/ \
    " --validate-trace             throw an error if the structure of the counterexample\n" /*NOLINT*/ \
    "                              trace does not match certain assumptions\n" /*NOLINT*/ \
    "                              (experimental, currently java only)\n" /*NOLINT*/ \

Definition at line 29 of file java_trace_validation.h.

◆ OPT_JAVA_TRACE_VALIDATION

#define OPT_JAVA_TRACE_VALIDATION

Value:

/*NOLINT*/ \

"(validate-trace)" \

Definition at line 26 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 121 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 127 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 85 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 94 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 328 of file java_trace_validation.cpp.

◆ get_inner_symbol_expr()

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, 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.

Macros

Functions