CBMC
dfcc_cfg_infot Member List

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_iddfcc_cfg_infotprivate
get_first_id_not_skipped_or_top_level_id(const std::size_t loop_id) constdfcc_cfg_infot
get_local_set(goto_programt::const_targett target) constdfcc_cfg_infot
get_loop_info(const std::size_t loop_id) constdfcc_cfg_infot
get_loops_toposorted() constdfcc_cfg_infotinline
get_outer_loop_identifier(const std::size_t loop_id) constdfcc_cfg_infot
get_outer_write_set(std::size_t loop_id) constdfcc_cfg_infot
get_top_level_tracked()dfcc_cfg_infotinline
get_top_level_write_set() constdfcc_cfg_infotinline
get_tracked_set(goto_programt::const_targett target) constdfcc_cfg_infot
get_write_set(goto_programt::const_targett target) constdfcc_cfg_infot
goto_functiondfcc_cfg_infotprivate
is_top_level_id(const std::size_t id) constdfcc_cfg_infotprivate
is_valid_loop_id(const std::size_t id) constdfcc_cfg_infotprivate
is_valid_loop_or_top_level_id(const std::size_t id) constdfcc_cfg_infotprivate
loop_info_mapdfcc_cfg_infotprivate
must_check_lhs(goto_programt::const_targett target) constdfcc_cfg_infot
must_track_decl_or_dead(goto_programt::const_targett target) constdfcc_cfg_infot
nsdfcc_cfg_infotprivate
output(std::ostream &out) constdfcc_cfg_infot
top_level_id() constdfcc_cfg_infotprivate
top_level_localdfcc_cfg_infotprivate
top_level_loopsdfcc_cfg_infotprivate
top_level_trackeddfcc_cfg_infotprivate
top_level_write_setdfcc_cfg_infotprivate
topsorted_loopsdfcc_cfg_infotprivate