CBMC
|
This is the complete list of members for dfcc_cfg_infot, including all inherited members.
dfcc_cfg_infot(goto_modelt &goto_model, const irep_idt &function_id, goto_functiont &goto_function, const exprt &top_level_write_set, const loop_contract_configt &loop_contract_config, symbol_table_baset &symbol_table, message_handlert &message_handler, dfcc_libraryt &library) | dfcc_cfg_infot | |
function_id | dfcc_cfg_infot | private |
get_first_id_not_skipped_or_top_level_id(const std::size_t loop_id) const | dfcc_cfg_infot | |
get_local_set(goto_programt::const_targett target) const | dfcc_cfg_infot | |
get_loop_info(const std::size_t loop_id) const | dfcc_cfg_infot | |
get_loops_toposorted() const | dfcc_cfg_infot | inline |
get_outer_loop_identifier(const std::size_t loop_id) const | dfcc_cfg_infot | |
get_outer_write_set(std::size_t loop_id) const | dfcc_cfg_infot | |
get_top_level_tracked() | dfcc_cfg_infot | inline |
get_top_level_write_set() const | dfcc_cfg_infot | inline |
get_tracked_set(goto_programt::const_targett target) const | dfcc_cfg_infot | |
get_write_set(goto_programt::const_targett target) const | dfcc_cfg_infot | |
goto_function | dfcc_cfg_infot | private |
is_top_level_id(const std::size_t id) const | dfcc_cfg_infot | private |
is_valid_loop_id(const std::size_t id) const | dfcc_cfg_infot | private |
is_valid_loop_or_top_level_id(const std::size_t id) const | dfcc_cfg_infot | private |
loop_info_map | dfcc_cfg_infot | private |
must_check_lhs(goto_programt::const_targett target) const | dfcc_cfg_infot | |
must_track_decl_or_dead(goto_programt::const_targett target) const | dfcc_cfg_infot | |
ns | dfcc_cfg_infot | private |
output(std::ostream &out) const | dfcc_cfg_infot | |
top_level_id() const | dfcc_cfg_infot | private |
top_level_local | dfcc_cfg_infot | private |
top_level_loops | dfcc_cfg_infot | private |
top_level_tracked | dfcc_cfg_infot | private |
top_level_write_set | dfcc_cfg_infot | private |
topsorted_loops | dfcc_cfg_infot | private |