24 "spawning threads out of atomic sections is not allowed; " 25 "this would require amendments to ordering constraints",
33 INVARIANT(instruction.
targets.size() == 1,
"start_thread expects one target");
39 std::size_t t=state.
threads.size();
43 new_thread.
pc=thread_target;
46 new_thread.
call_stack.back().local_objects.clear();
47 new_thread.
call_stack.back().goto_state_map.clear();
49 new_thread.abstract_events=&(
target.new_thread(cur_thread.abstract_events));
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);
100 for(
const auto &symbol_pair : symbol_table.
symbols)
102 const symbolt &symbol = symbol_pair.second;
virtual void spawn(const exprt &guard, const sourcet &source)
Record spawning a new thread.
goto_programt::const_targett pc
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
bool is_false() const
Return whether the expression is a constant representing false.
exprt value
Initial value of symbol.
#define CHECK_RETURN(CONDITION)
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
targetst targets
The list of successor instructions.
This class represents an instruction in the GOTO intermediate representation.
goto_programt::const_targett pc
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Expression Initialization.
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
void set_level_0(unsigned i)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
std::set< irep_idt > l1_history
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
symex_target_equationt & target
instructionst::const_iterator const_targett
std::vector< threadt > threads
current_namest current_names
std::set< irep_idt > local_objects
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
unsigned atomic_section_id
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
Base class for all expressions.
#define UNREACHABLE
This should be used to mark dead code.
virtual void symex_start_thread(statet &)
Expression providing an SSA-renamed symbol of expressions.
symex_targett::sourcet source
void symex_assign_symbol(statet &, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)