java_trace_validation.cpp File Reference

#include "java_trace_validation.h"
#include <algorithm>
#include <goto-programs/goto_trace.h>
#include <util/byte_operators.h>
#include <util/expr_util.h>
#include <util/pointer_expr.h>
#include <util/simplify_expr.h>
#include <util/std_expr.h>

Include dependency graph for java_trace_validation.cpp:

Go to the source code of this file.

Functions
bool	check_symbol_structure (const exprt &expr)
static bool	may_be_lvalue (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)
static bool	check_annotated_pointer_constant_structure (const annotated_pointer_constant_exprt &constant_expr)
static void	check_lhs_assumptions (const exprt &lhs, const namespacet &ns, const validation_modet vm)
static void	check_rhs_assumptions (const exprt &rhs, const namespacet &ns, const validation_modet vm)
static void	check_step_assumptions (const goto_trace_stept &step, const namespacet &ns, const validation_modet vm)
void	check_trace_assumptions (const goto_tracet &trace, const namespacet &ns, const messaget &log, const bool run_check, const validation_modet vm)
	Checks that the structure of each step of the trace matches certain criteria.

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_annotated_pointer_constant_structure()

static bool check_annotated_pointer_constant_structure ( const annotated_pointer_constant_exprt &  constant_expr )

static

Definition at line 133 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_lhs_assumptions()

static void check_lhs_assumptions ( const exprt &  lhs, const namespacet &  ns, const validation_modet  vm  )

static

Definition at line 142 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_rhs_assumptions()

static void check_rhs_assumptions ( const exprt &  rhs, const namespacet &  ns, const validation_modet  vm  )

static

Definition at line 206 of file java_trace_validation.cpp.

check_step_assumptions()

static void check_step_assumptions ( const goto_trace_stept &  step, const namespacet &  ns, const validation_modet  vm  )

static

Definition at line 303 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.

may_be_lvalue()

static bool may_be_lvalue ( const exprt &  expr )

static

Returns

true iff the expression is a symbol or is an expression whose first operand can contain a nested symbol

Definition at line 29 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.