goto_functionst Class Reference

#include <goto_functions.h>

Classes
struct	id_string_order
	Order function_map by the id's string content, not by irep_idt's default operator< (which compares the string-pool interning index). More...

Public Types
typedef std::map< irep_idt, goto_functiont, id_string_order >	function_mapt

Public Member Functions
void	clear ()
void	output (const namespacet &ns, std::ostream &out) const
void	dump () const
void	compute_location_numbers ()
void	compute_loop_numbers ()
void	compute_target_numbers ()
void	update ()
irep_idt	main_id () const
void	swap (goto_functionst &other)

Public Attributes
function_mapt	function_map

Static Public Attributes
static std::unordered_set< std::string >	reached_claims
static std::unordered_multiset< std::string >	reached_mul_claims
static std::mutex	reached_claims_mutex
static std::mutex	reached_mul_claims_mutex
static property_verdict_tablet	property_verdicts
static std::mutex	clear_claims_mutex

Member Typedef Documentation

function_mapt

typedef std::map<irep_idt, goto_functiont, id_string_order> goto_functionst::function_mapt

Member Function Documentation

clear()

void goto_functionst::clear ( )

inline

compute_location_numbers()

void goto_functionst::compute_location_numbers

(

)

compute_loop_numbers()

void goto_functionst::compute_loop_numbers

(

)

compute_target_numbers()

void goto_functionst::compute_target_numbers

(

)

dump()

void goto_functionst::dump

(

)

const

main_id()

irep_idt goto_functionst::main_id ( ) const

inline

output()

void goto_functionst::output	(	const namespacet &	ns,
		std::ostream &	out ) const

swap()

void goto_functionst::swap ( goto_functionst & other )

inline

update()

void goto_functionst::update ( )

inline

Member Data Documentation

clear_claims_mutex

std::mutex goto_functionst::clear_claims_mutex

static

function_map

function_mapt goto_functionst::function_map

property_verdicts

property_verdict_tablet goto_functionst::property_verdicts

static

reached_claims

std::unordered_set< std::string > goto_functionst::reached_claims

static

reached_claims_mutex

std::mutex goto_functionst::reached_claims_mutex

static

reached_mul_claims

std::unordered_multiset< std::string > goto_functionst::reached_mul_claims

static

reached_mul_claims_mutex

std::mutex goto_functionst::reached_mul_claims_mutex

static

---

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

• src/goto-programs/goto_functions.h
• src/esbmc/bmc.cpp
• src/goto-programs/goto_function.cpp
• src/goto-programs/property_verdict.cpp