w_guardst Class Reference

Public Member Functions
	w_guardst (contextt &_context)
expr2tc	get_w_guard_expr (const rw_sett::entryt &entry)
expr2tc	get_assertion (const rw_sett::entryt &entry)
void	add_initialization (goto_programt &goto_program)

Protected Member Functions
expr2tc	get_guard_symbol_expr (const expr2tc &original_expr)

Protected Attributes
contextt &	context

Constructor & Destructor Documentation

w_guardst()

w_guardst::w_guardst ( contextt & _context )

inlineexplicit

Member Function Documentation

add_initialization()

void w_guardst::add_initialization

(

goto_programt &

goto_program

)

get_assertion()

expr2tc w_guardst::get_assertion ( const rw_sett::entryt & entry )

inline

get_guard_symbol_expr()

expr2tc w_guardst::get_guard_symbol_expr ( const expr2tc & original_expr )

inlineprotected

get_w_guard_expr()

expr2tc w_guardst::get_w_guard_expr ( const rw_sett::entryt & entry )

inline

Member Data Documentation

context

contextt& w_guardst::context

protected

---

The documentation for this class was generated from the following file:

• src/goto-programs/add_race_assertions.cpp