20 if(instruction.is_start_thread())
36 assert(end->is_end_function());
52 end->source_location_nonconst().set_comment(
53 "mutexes must not be locked on thread exit");
67 for(
const auto &instruction :
gf_entry.second.body.instructions)
68 if(instruction.is_function_call())
70 const exprt &function = instruction.call_function();
88 symbol_tablet::symbolst::const_iterator
f_it =
101 f_it->second.symbol_expr(),
102 {address_of_exprt(it->assign_lhs()),
103 address_of_exprt(string_constantt(
"mutex-init"))});
116 symbol_tablet::symbolst::const_iterator
lock_entry =
void base_type(typet &type, const namespacet &ns)
pointer_typet pointer_type(const typet &subtype)
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
codet representation of a function call statement.
Base class for all expressions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::iterator targett
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
const irep_idt & id() const
The null pointer constant.
const irep_idt & get_identifier() const
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The type of an expression, extends irept.
#define Forall_goto_program_instructions(it, program)
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
void thread_exit_instrumentation(goto_programt &goto_program)
void mutex_init_instrumentation(const symbol_tablet &symbol_table, goto_programt &goto_program, typet lock_type)
static bool has_start_thread(const goto_programt &goto_program)