CBMC
Public Member Functions | Protected Types | Protected Member Functions | Static Protected Member Functions | Protected Attributes | List of all members
state_encodingt Class Reference
+ Collaboration diagram for state_encodingt:

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 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: