CBMC: /home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_trace_validation.cpp File Reference

CBMC

Loading...

Searching...

No Matches

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.