ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
goto_atomicity_check.h
Go to the documentation of this file.
1#ifndef GOTO_PROGRAMS_GOTO_ATOMICITY_CHECK_H_
2#define GOTO_PROGRAMS_GOTO_ATOMICITY_CHECK_H_
3
4#include <goto-programs/goto_functions.h>
5#include <util/symtab/context.h>
6#include <util/symtab/namespace.h>
7
18void goto_atomicity_check(
19 goto_functionst &goto_functions,
20 const namespacet &ns,
21 contextt &context);
22
23#endif // GOTO_PROGRAMS_GOTO_ATOMICITY_CHECK_H_
contextt
Definition context.h:57
goto_functionst
Definition goto_functions.h:56
namespacet
Definition namespace.h:10
goto_atomicity_check
void goto_atomicity_check(goto_functionst &goto_functions, const namespacet &ns, contextt &context)
Post-GOTO-conversion atomicity check instrumentation pass.
Definition goto_atomicity_check.cpp:309
goto_functions.h