goto_atomicity_checkt Class Reference

Public Member Functions
	goto_atomicity_checkt (const namespacet &_ns, contextt &_context)
void	check (goto_programt &program)
	Instruments all ASSIGN, ASSERT, ASSUME, GOTO, and RETURN instructions in program that reference global variables, inserting snapshot temporaries and atomicity assertions.

Constructor & Destructor Documentation

goto_atomicity_checkt()

goto_atomicity_checkt::goto_atomicity_checkt ( const namespacet & _ns, contextt & _context )

inline

Member Function Documentation

check()

void goto_atomicity_checkt::check

(

goto_programt &

program

)

Instruments all ASSIGN, ASSERT, ASSUME, GOTO, and RETURN instructions in program that reference global variables, inserting snapshot temporaries and atomicity assertions.

---

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

• src/goto-programs/goto_atomicity_check.cpp