Loading...

Searching...

No Matches

state_encodingt Class Reference

+ Collaboration diagram for state_encodingt:

[フレーム]

[legend]

Public Member Functions

state_encodingt (const goto_modelt &__goto_model)

void operator() (const goto_functionst::function_mapt::const_iterator, encoding_targett &)

void encode (const goto_functiont &, const irep_idt function_identifier, const std::string &state_prefix, const std::vector< irep_idt > &call_stack, const std::string &annotation, const symbol_exprt &entry_state, const exprt &return_lhs, encoding_targett &)

state_encodingt (const goto_functionst &__goto_functions)

void operator() (const goto_functionst::function_mapt::const_iterator, encoding_targett &)

void encode (const goto_functiont &, const std::string &state_prefix, const std::string &annotation, const symbol_exprt &entry_state, const exprt &return_lhs, encoding_targett &)

Protected Types

using loct = goto_programt::const_targett

using incomingt = std::map< loct, std::vector< loct >, goto_programt::target_less_than >

using loct = goto_programt::const_targett

using incomingt = std::map< loct, std::vector< loct >, goto_programt::target_less_than >

Protected Member Functions

symbol_exprt out_state_expr (loct) const

symbol_exprt state_expr_with_suffix (loct, const std::string &suffix) const

symbol_exprt out_state_expr (loct, bool taken) const

symbol_exprt in_state_expr (loct) const

std::vector< symbol_exprt > incoming_symbols (loct) const

exprt evaluate_expr (loct, const exprt &, const exprt &) const

exprt evaluate_expr_rec (loct, const exprt &, const exprt &, const std::unordered_set< symbol_exprt, irep_hash > &) const

exprt replace_nondet_rec (loct, const exprt &, std::vector< symbol_exprt > &nondet_symbols) const

exprt evaluate_expr (loct, const exprt &) const

exprt address_rec (loct, const exprt &, exprt) const

exprt forall_states_expr (loct, exprt) const

exprt forall_states_expr (loct, exprt, exprt) const

void setup_incoming (const goto_functiont &)

exprt assignment_constraint (loct, exprt lhs, exprt rhs) const

exprt assignment_constraint_rec (loct, exprt state, exprt lhs, exprt rhs, std::vector< symbol_exprt > &nondet_symbols) const

void function_call (goto_programt::const_targett, encoding_targett &)

void function_call_symbol (goto_programt::const_targett, encoding_targett &)

symbol_exprt out_state_expr (loct) const

symbol_exprt state_expr_with_suffix (loct, const std::string &suffix) const

symbol_exprt out_state_expr (loct, bool taken) const

symbol_exprt in_state_expr (loct) const

std::vector< symbol_exprt > incoming_symbols (loct) const

exprt evaluate_expr (loct, const exprt &, const exprt &) const

exprt evaluate_expr_rec (loct, const exprt &, const exprt &, const std::unordered_set< symbol_exprt, irep_hash > &) const

exprt replace_nondet_rec (loct, const exprt &, std::vector< symbol_exprt > &nondet_symbols) const

exprt evaluate_expr (loct, const exprt &) const

exprt address_rec (loct, const exprt &, exprt) const

exprt forall_states_expr (loct, exprt) const

exprt forall_states_expr (loct, exprt, exprt) const

void setup_incoming (const goto_functiont &)

exprt assignment_constraint (loct, exprt lhs, exprt rhs) const

void function_call (goto_programt::const_targett, encoding_targett &)

void function_call_symbol (goto_programt::const_targett, encoding_targett &)

Static Protected Member Functions

static exprt state_lambda_expr (exprt)

static symbol_exprt va_args (irep_idt function)

static exprt state_lambda_expr (exprt)

Protected Attributes

const goto_modelt & goto_model

irep_idt function_identifier

std::string state_prefix

std::string annotation

std::vector< irep_idt > call_stack

loct first_loc

symbol_exprt entry_state = symbol_exprt(irep_idt(), typet())

exprt return_lhs = nil_exprt()

incomingt incoming

const goto_functionst & goto_functions

Detailed Description

Definition at line 32 of file state_encoding.cpp.

Member Typedef Documentation

◆ incomingt [1/2]

using state_encodingt::incomingt = std::map<loct, std::vector<loct>, goto_programt::target_less_than>

protected

Definition at line 96 of file state_encoding.cpp.

◆ incomingt [2/2]

using state_encodingt::incomingt = std::map<loct, std::vector<loct>, goto_programt::target_less_than>

protected

Definition at line 392 of file horn_encoding.cpp.

◆ loct [1/2]

using state_encodingt::loct = goto_programt::const_targett

protected

Definition at line 55 of file state_encoding.cpp.

◆ loct [2/2]

using state_encodingt::loct = goto_programt::const_targett

protected

Definition at line 359 of file horn_encoding.cpp.

Constructor & Destructor Documentation

◆ state_encodingt() [1/2]

state_encodingt::state_encodingt ( const goto_modelt & __goto_model )

inlineexplicit

Definition at line 35 of file state_encoding.cpp.

◆ state_encodingt() [2/2]

state_encodingt::state_encodingt ( const goto_functionst & __goto_functions )

inlineexplicit

Definition at line 341 of file horn_encoding.cpp.

Member Function Documentation

◆ address_rec() [1/2]

exprt state_encodingt::address_rec ( loct loc,

const exprt & state,

exprt expr

) const

protected

Definition at line 412 of file state_encoding.cpp.

◆ address_rec() [2/2]

exprt state_encodingt::address_rec ( loct ,

const exprt & ,

exprt

) const

protected

◆ assignment_constraint() [1/2]

exprt state_encodingt::assignment_constraint ( loct loc,

exprt lhs,

exprt rhs

) const

protected

Definition at line 588 of file state_encoding.cpp.

◆ assignment_constraint() [2/2]

exprt state_encodingt::assignment_constraint ( loct ,

exprt lhs,

exprt rhs

) const

protected

◆ assignment_constraint_rec()

exprt state_encodingt::assignment_constraint_rec ( loct loc,

exprt state,

exprt lhs,

exprt rhs,

std::vector< symbol_exprt > & nondet_symbols

) const

protected

Definition at line 502 of file state_encoding.cpp.

◆ encode() [1/2]

void state_encodingt::encode ( const goto_functiont & goto_function,

const irep_idt function_identifier,

const std::string & state_prefix,

const std::vector< irep_idt > & call_stack,

const std::string & annotation,

const symbol_exprt & entry_state,

const exprt & return_lhs,

encoding_targett & dest

)

Definition at line 929 of file state_encoding.cpp.

◆ encode() [2/2]

void state_encodingt::encode ( const goto_functiont & goto_function,

const std::string & state_prefix,

const std::string & annotation,

const symbol_exprt & entry_state,

const exprt & return_lhs,

encoding_targett & dest

)

Definition at line 841 of file horn_encoding.cpp.

◆ evaluate_expr() [1/4]

exprt state_encodingt::evaluate_expr ( loct loc,

const exprt & what

) const

protected

Definition at line 381 of file state_encoding.cpp.

◆ evaluate_expr() [2/4]

exprt state_encodingt::evaluate_expr ( loct ,

const exprt &

) const

protected

◆ evaluate_expr() [3/4]

exprt state_encodingt::evaluate_expr ( loct loc,

const exprt & state,

const exprt & what

) const

protected

Definition at line 162 of file state_encoding.cpp.

◆ evaluate_expr() [4/4]

exprt state_encodingt::evaluate_expr ( loct ,

const exprt & ,

const exprt &

) const

protected

◆ evaluate_expr_rec() [1/2]

exprt state_encodingt::evaluate_expr_rec ( loct loc,

const exprt & state,

const exprt & what,

const std::unordered_set< symbol_exprt, irep_hash > & bound_symbols

) const

protected

Definition at line 207 of file state_encoding.cpp.

◆ evaluate_expr_rec() [2/2]

exprt state_encodingt::evaluate_expr_rec ( loct ,

const exprt & ,

const std::unordered_set< symbol_exprt, irep_hash > &

) const

protected

◆ forall_states_expr() [1/4]

exprt state_encodingt::forall_states_expr ( loct loc,

exprt what

) const

protected

Definition at line 391 of file state_encoding.cpp.

◆ forall_states_expr() [2/4]

exprt state_encodingt::forall_states_expr ( loct ,

exprt

) const

protected

◆ forall_states_expr() [3/4]

exprt state_encodingt::forall_states_expr ( loct loc,

exprt condition,

exprt what

) const

protected

Definition at line 400 of file state_encoding.cpp.

◆ forall_states_expr() [4/4]

exprt state_encodingt::forall_states_expr ( loct ,

exprt ,

exprt

) const

protected

◆ function_call() [1/2]

void state_encodingt::function_call ( goto_programt::const_targett loc,

encoding_targett & dest

)

protected

Definition at line 875 of file state_encoding.cpp.

◆ function_call() [2/2]

void state_encodingt::function_call ( goto_programt::const_targett ,

encoding_targett &

)

protected

◆ function_call_symbol() [1/2]

void state_encodingt::function_call_symbol ( goto_programt::const_targett loc,

encoding_targett & dest

)

protected

Definition at line 647 of file state_encoding.cpp.

◆ function_call_symbol() [2/2]

void state_encodingt::function_call_symbol ( goto_programt::const_targett ,

encoding_targett &

)

protected

◆ in_state_expr() [1/2]

symbol_exprt state_encodingt::in_state_expr ( loct loc ) const

protected

Definition at line 149 of file state_encoding.cpp.

◆ in_state_expr() [2/2]

symbol_exprt state_encodingt::in_state_expr ( loct ) const

protected

◆ incoming_symbols() [1/2]

std::vector< symbol_exprt > state_encodingt::incoming_symbols ( loct loc ) const

protected

Definition at line 122 of file state_encoding.cpp.

◆ incoming_symbols() [2/2]

std::vector< symbol_exprt > state_encodingt::incoming_symbols ( loct ) const

protected

◆ operator()() [1/2]

void state_encodingt::operator() ( const goto_functionst::function_mapt::const_iterator f_entry,

encoding_targett & dest

)

Definition at line 898 of file state_encoding.cpp.

◆ operator()() [2/2]

void state_encodingt::operator() ( const goto_functionst::function_mapt::const_iterator ,

encoding_targett &

)

◆ out_state_expr() [1/4]

symbol_exprt state_encodingt::out_state_expr ( loct loc ) const

protected

Definition at line 103 of file state_encoding.cpp.

◆ out_state_expr() [2/4]

symbol_exprt state_encodingt::out_state_expr ( loct ) const

protected

◆ out_state_expr() [3/4]

symbol_exprt state_encodingt::out_state_expr ( loct loc,

bool taken

) const

protected

Definition at line 117 of file state_encoding.cpp.

◆ out_state_expr() [4/4]

symbol_exprt state_encodingt::out_state_expr ( loct ,

bool taken

) const

protected

◆ replace_nondet_rec() [1/2]

exprt state_encodingt::replace_nondet_rec ( loct loc,

const exprt & what,

std::vector< symbol_exprt > & nondet_symbols

) const

protected

Definition at line 170 of file state_encoding.cpp.

◆ replace_nondet_rec() [2/2]

exprt state_encodingt::replace_nondet_rec ( loct ,

const exprt & ,

std::vector< symbol_exprt > & nondet_symbols

) const

protected

◆ setup_incoming() [1/2]

void state_encodingt::setup_incoming ( const goto_functiont & goto_function )

protected

Definition at line 606 of file state_encoding.cpp.

◆ setup_incoming() [2/2]

void state_encodingt::setup_incoming ( const goto_functiont & )

protected

◆ state_expr_with_suffix() [1/2]

symbol_exprt state_encodingt::state_expr_with_suffix ( loct loc,

const std::string & suffix

) const

protected

Definition at line 108 of file state_encoding.cpp.

◆ state_expr_with_suffix() [2/2]

symbol_exprt state_encodingt::state_expr_with_suffix ( loct ,

const std::string & suffix

) const

protected

◆ state_lambda_expr() [1/2]

exprt state_encodingt::state_lambda_expr ( exprt what )

staticprotected

Definition at line 386 of file state_encoding.cpp.

◆ state_lambda_expr() [2/2]

static exprt state_encodingt::state_lambda_expr ( exprt )

staticprotected

◆ va_args()

symbol_exprt state_encodingt::va_args ( irep_idt function )

staticprotected

Definition at line 638 of file state_encoding.cpp.

Member Data Documentation

◆ annotation

std::string state_encodingt::annotation

protected

Definition at line 91 of file state_encoding.cpp.

◆ call_stack

std::vector<irep_idt> state_encodingt::call_stack

protected

Definition at line 92 of file state_encoding.cpp.

◆ entry_state

symbol_exprt state_encodingt::entry_state = symbol_exprt(irep_idt(), typet())

protected

Definition at line 94 of file state_encoding.cpp.

◆ first_loc

loct state_encodingt::first_loc

protected

Definition at line 93 of file state_encoding.cpp.

◆ function_identifier

irep_idt state_encodingt::function_identifier

protected

Definition at line 89 of file state_encoding.cpp.

◆ goto_functions

const goto_functionst& state_encodingt::goto_functions

protected

Definition at line 360 of file horn_encoding.cpp.

◆ goto_model

const goto_modelt& state_encodingt::goto_model

protected

Definition at line 56 of file state_encoding.cpp.

◆ incoming

incomingt state_encodingt::incoming

protected

Definition at line 98 of file state_encoding.cpp.

◆ return_lhs

exprt state_encodingt::return_lhs = nil_exprt()

protected

Definition at line 95 of file state_encoding.cpp.

◆ state_prefix

std::string state_encodingt::state_prefix

protected

Definition at line 90 of file state_encoding.cpp.

The documentation for this class was generated from the following files:

/home/runner/work/cbmc/cbmc/src/cprover/state_encoding.cpp
/home/runner/work/cbmc/cbmc/src/goto-instrument/horn_encoding.cpp