goto_function.cpp File Reference

#include <cassert>
#include <goto-programs/goto_convert_class.h>
#include <goto-programs/goto_functions.h>
#include <util/lang/c_types.h>
#include <util/symtab/cprover_prefix.h>
#include <util/expr/expr_util.h>
#include <util/base/i2string.h>
#include <util/irep/location.h>
#include <util/base/prefix.h>

Include dependency graph for goto_function.cpp:

Functions
void	get_local_identifiers (const goto_functiont &goto_function, std::set< irep_idt > &dest)
static void	collect_taken_functions (const expr2tc &e, const goto_functionst &goto_functions, std::vector< irep_idt > &out)
	Every function whose address e takes, restricted to names that are functions.
bool	spawns_threads (const goto_functionst &goto_functions)
	Whether the program can create a thread.

Function Documentation

collect_taken_functions()

void collect_taken_functions ( const expr2tc & e, const goto_functionst & goto_functions, std::vector< irep_idt > & out )

static

Every function whose address e takes, restricted to names that are functions.

A thread's start routine is reached no other way.

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.