17 if(instruction.is_start_thread())
33 assert(end->is_end_function());
40 exprt mutex_locked_string=
51 end->source_location=source_location;
52 end->source_location.set_comment(
"mutexes must not be locked on thread exit");
53 end->function=
function;
59 std::set<irep_idt> thread_fkts;
67 for(
const auto &instruction : f_it->second.body.instructions)
68 if(instruction.is_function_call())
70 const exprt &
function=
72 if(
function.
id()==ID_symbol)
79 for(
const auto &fkt : thread_fkts)
90 symbol_tablet::symbolst::const_iterator f_it=
91 symbol_table.
symbols.find(
"__CPROVER_set_must");
93 if(f_it==symbol_table.
symbols.end())
103 if(code_assign.
lhs().
type()==lock_type)
109 call.
function()=f_it->second.symbol_expr();
114 t->make_function_call(call);
115 t->source_location=it->source_location;
127 symbol_tablet::symbolst::const_iterator f_it=
128 symbol_table.
symbols.find(
"pthread_mutex_lock");
130 if(f_it==symbol_table.
symbols.end())
140 if(lock_type.
id()!=ID_pointer)
145 symbol_table, f_it->second.body, lock_type.
subtype());
The type of an expression.
pointer_typet pointer_type(const typet &subtype)
void mutex_init_instrumentation(const symbol_tablet &symbol_table, goto_programt &goto_program, typet lock_type)
instructionst instructions
The list of instructions in the goto program.
The null pointer constant.
static bool has_start_thread(const goto_programt &goto_program)
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
A generic base class for binary expressions.
targett insert_after(const_targett target)
Insertion after the given target.
Operator to return the address of an object.
function_mapt function_map
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Base class for all expressions.
const parameterst & parameters() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
#define Forall_goto_functions(it, functions)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
#define Forall_goto_program_instructions(it, program)
const typet & subtype() const
#define forall_goto_functions(it, functions)
const code_function_callt & to_code_function_call(const codet &code)
void thread_exit_instrumentation(goto_programt &goto_program)
instructionst::iterator targett