28 "spawning threads out of atomic sections is not allowed; "
29 "this would require amendments to ordering constraints",
37 INVARIANT(instruction.
targets.size() == 1,
"start_thread expects one target");
43 const std::size_t new_thread_nr = state.
threads.size();
47 new_thread.
pc=thread_target;
51 new_thread.
call_stack.back().local_objects.clear();
52 new_thread.
call_stack.back().goto_state_map.clear();
54 new_thread.abstract_events=&(
target.new_thread(cur_thread.abstract_events));
65 for(
const auto &pair : view)
67 const irep_idt l1_o_id = pair.second.first.get_l1_object_identifier();
74 ssa_exprt lhs(pair.second.first.get_original_expr());
79 const irep_idt &l0_name = l0_lhs.
get().get_identifier();
80 std::size_t l1_index = path_storage.get_unique_l1_index(l0_name, 0);
89 new_thread.
call_stack.back().local_objects.insert(l1_name);
124 for(
const auto &symbol_pair : symbol_table.
symbols)
126 const symbolt &symbol = symbol_pair.second;
Expression in which some part is missing and can be substituted for another expression.
Base class for all expressions.
std::vector< exprt > operandst
Stack frames – these are used for function calls and for exceptions.
std::set< irep_idt > local_objects
This class represents an instruction in the GOTO intermediate representation.
targetst targets
The list of successor instructions.
const_targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
instructionst::const_iterator const_targett
bool reachable
Is this code reachable?
unsigned atomic_section_id
Threads.
const symex_level2t & get_level2() const
call_stackt & call_stack()
std::stack< bool > record_events
renamedt< exprt, level > rename(exprt expr, const namespacet &ns)
Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...
write_is_shared_resultt write_is_shared(const ssa_exprt &expr, const namespacet &ns) const
symex_targett::sourcet source
renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
std::vector< threadt > threads
goto_symex_statet statet
A type abbreviation for goto_symex_statet.
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
symex_target_equationt & target
The equation that this execution is building up.
guard_managert & guard_manager
Used to create guards.
shadow_memoryt shadow_memory
Shadow memory instrumentation API.
virtual void symex_start_thread(statet &state)
Symbolically execute a START_THREAD instruction.
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
const symex_configt symex_config
The configuration to use for this symbolic execution.
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
Wrapper for expressions or types which have been renamed up to a given level.
const underlyingt & get() const
std::vector< view_itemt > viewt
void get_view(V &view) const
Get a view of the elements in the map A view is a list of pairs with the components being const refer...
Expression providing an SSA-renamed symbol of expressions.
const irep_idt get_l1_object_identifier() const
void set_level_0(std::size_t i)
const symbolst & symbols
Read-only field, used to look up symbols given their names.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
exprt value
Initial value of symbol.
Functor for symex assignment.
void assign_symbol(const ssa_exprt &lhs, const expr_skeletont &full_lhs, const exprt &rhs, const exprt::operandst &guard)
Record the assignment of value rhs to variable lhs in state and add the equation to target: lhs#{n+1}...
std::optional< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
Storage of symbolic execution paths to resume.
renamedt< ssa_exprt, L0 > symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr)
Set the level 0 renaming of SSA expressions.
#define CHECK_RETURN(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
bool is_ssa_expr(const exprt &expr)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
goto_programt::const_targett pc
void insert(const renamedt< ssa_exprt, L0 > &ssa, std::size_t index)
Assume ssa is not already known.
symex_renaming_levelt current_names
goto_programt::const_targett pc
Symbolic Execution of assignments.