reachability_tree.cpp File Reference

#include <goto-programs/goto_functions.h>
#include <goto-symex/engine/goto_symex.h>
#include <goto-symex/scheduler/reachability_tree.h>
#include <irep2/irep2_expr.h>
#include <util/config/config.h>
#include <util/expr/expr_util.h>
#include <util/base/i2string.h>
#include <util/base/prefix.h>
#include <util/message/message.h>
#include <util/irep/std_expr.h>

Include dependency graph for reachability_tree.cpp:

Functions
static void	add_if_global (const irep_idt &name, const namespacet &ns, std::unordered_set< irep_idt, irep_id_hash > &out)
static void	collect_write_targets (const expr2tc &e, const namespacet &ns, std::unordered_set< irep_idt, irep_id_hash > &out, bool &indirect_write)
static void	collect_object_root (const expr2tc &e, const namespacet &ns, std::unordered_set< irep_idt, irep_id_hash > &globals, std::unordered_set< irep_idt, irep_id_hash > &locals)
static void	collect_address_taken (const expr2tc &e, const namespacet &ns, std::unordered_set< irep_idt, irep_id_hash > &globals, std::unordered_set< irep_idt, irep_id_hash > &locals)
static irep_idt	called_function_name (const goto_programt::instructiont &ins)
static std::unordered_set< irep_idt, irep_id_hash >	compute_thread_spawners (const goto_functionst &goto_functions)
static std::unordered_set< const goto_programt::instructiont * >	instructions_after_spawn (const goto_programt &body, const std::unordered_set< irep_idt, irep_id_hash > &spawners)

Function Documentation

add_if_global()

void add_if_global ( const irep_idt & name, const namespacet & ns, std::unordered_set< irep_idt, irep_id_hash > & out )

static

called_function_name()

irep_idt called_function_name ( const goto_programt::instructiont & ins )

static

collect_address_taken()

void collect_address_taken ( const expr2tc & e, const namespacet & ns, std::unordered_set< irep_idt, irep_id_hash > & globals, std::unordered_set< irep_idt, irep_id_hash > & locals )

static

collect_object_root()

void collect_object_root ( const expr2tc & e, const namespacet & ns, std::unordered_set< irep_idt, irep_id_hash > & globals, std::unordered_set< irep_idt, irep_id_hash > & locals )

static

collect_write_targets()

void collect_write_targets ( const expr2tc & e, const namespacet & ns, std::unordered_set< irep_idt, irep_id_hash > & out, bool & indirect_write )

static

compute_thread_spawners()

std::unordered_set< irep_idt, irep_id_hash > compute_thread_spawners ( const goto_functionst & goto_functions )

static

instructions_after_spawn()

std::unordered_set< const goto_programt::instructiont * > instructions_after_spawn ( const goto_programt & body, const std::unordered_set< irep_idt, irep_id_hash > & spawners )

static