goto_functions.h File Reference

#include <goto-programs/goto_program.h>
#include <goto-programs/property_verdict.h>
#include <util/irep/std_types.h>
#include <util/config/options.h>
#include <util/lang/exception_specification.h>

Include dependency graph for goto_functions.h:

Go to the source code of this file.

Classes
class	goto_functiont
class	goto_functionst
struct	goto_functionst::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...

Macros
#define	Forall_goto_functions(it, functions)
#define	forall_goto_functions(it, functions)

Functions
void	get_local_identifiers (const goto_functiont &, std::set< irep_idt > &dest)
bool	spawns_threads (const goto_functionst &goto_functions)
	Whether the program can create a thread.

Macro Definition Documentation

Forall_goto_functions

#define Forall_goto_functions	(		it,
			functions )

Value:

  for (goto_functionst::function_mapt::iterator it =                           \
         (functions).function_map.begin();                                     \
       it != (functions).function_map.end();                                   \
       it++)

forall_goto_functions

#define forall_goto_functions	(		it,
			functions )

Value:

  for (goto_functionst::function_mapt::const_iterator it =                     \
         (functions).function_map.begin();                                     \
       it != (functions).function_map.end();                                   \
       it++)

Function Documentation

get_local_identifiers()

void get_local_identifiers	(	const goto_functiont &	goto_function,
		std::set< irep_idt > &	dest )

spawns_threads()

bool spawns_threads

(

const goto_functionst &

goto_functions

)

Whether the program can create a thread.

Every route – pthread_create, std::thread, a CUDA kernel launch, threading.Thread – lowers to the __ESBMC_spawn_thread intrinsic, so reaching it is the creation point. Reachability and not presence: pthread_lib.c is linked into every program. An indirect call needs no special case: symex resolves one through the value set into a list of concrete symbols (get_function_list in symex_function.cpp), so it can only reach a function whose address is taken somewhere – which is exactly what collect_taken_functions seeds the worklist with.