24 throw "start_thread in atomic section detected";
29 const goto_programt::instructiont &instruction=*state.
source.
pc;
31 if(instruction.targets.size()!=1)
32 throw "start_thread expects one target";
35 instruction.targets.front();
38 std::size_t t=state.
threads.size();
42 new_thread.
pc=thread_target;
45 new_thread.
call_stack.back().local_objects.clear();
46 new_thread.
call_stack.back().goto_state_map.clear();
48 new_thread.abstract_events=&(
target.new_thread(cur_thread.abstract_events));
54 for(goto_symex_statet::renaming_levelt::current_namest::const_iterator
59 const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
65 ssa_exprt lhs(c_it->second.first.get_original_expr());
72 std::make_pair(lhs.get_l1_object_identifier(),
73 std::make_pair(lhs, 0))).second)
76 const irep_idt l1_name=lhs.get_l1_object_identifier();
79 new_thread.
call_stack.back().local_objects.insert(l1_name);
102 const symbolt &symbol=it->second;
Linking: Zero Initialization.
goto_programt::const_targett pc
#define forall_symbols(it, expr)
const symbol_tablet & get_symbol_table() const
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
exprt value
Initial value of symbol.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
goto_symex_statet::level2t level2
void symex_assign_symbol(statet &state, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
instructionst::const_iterator const_targett
void set_level_0(unsigned i)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
local_objectst local_objects
virtual void spawn(const exprt &guard, const sourcet &source)=0
virtual void symex_start_thread(statet &state)
goto_symex_statet::level1t level1
current_namest current_names
unsigned atomic_section_id
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
Base class for all expressions.
goto_programt::const_targett pc
Expression providing an SSA-renamed symbol of expressions.
symex_targett::sourcet source