goto_atomicity_check.cpp File Reference

#include <goto-programs/goto_atomicity_check.h>
#include <irep2/irep2_expr.h>
#include <irep2/irep2_utils.h>
#include <util/irep/migrate.h>
#include <util/symtab/symbol_generator.h>

Include dependency graph for goto_atomicity_check.cpp:

Classes
class	goto_atomicity_checkt

Functions
static expr2tc	make_conjunction (const std::vector< expr2tc > &conjuncts)
void	goto_atomicity_check (goto_functionst &goto_functions, const namespacet &ns, contextt &context)
	Post-GOTO-conversion atomicity check instrumentation pass.

Function Documentation

goto_atomicity_check()

void goto_atomicity_check	(	goto_functionst &	goto_functions,
		const namespacet &	ns,
		contextt &	context )

Post-GOTO-conversion atomicity check instrumentation pass.

For each assignment to or read from a global variable, inserts:

• Snapshot assignments: tmp_i = global_i
• If the LHS is also a global: ATOMIC_BEGIN ... ATOMIC_END wrapping
• An assertion: assert(tmp_i == global_i) checking for concurrent modification between the snapshot and the assignment.

This corresponds to the –atomicity-check flag and detects violations of atomicity when multiple threads access shared global variables.

make_conjunction()

expr2tc make_conjunction ( const std::vector< expr2tc > & conjuncts )

static