ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
goto_termination.h
Go to the documentation of this file.
1#ifndef GOTO_PROGRAMS_GOTO_TERMINATION_H_
2#define GOTO_PROGRAMS_GOTO_TERMINATION_H_
3
4#include <goto-programs/goto_functions.h>
5#include <util/symtab/namespace.h>
6#include <util/config/options.h>
7
33void goto_termination(
34 goto_functionst &goto_functions,
35 optionst &options,
36 const namespacet &ns);
37
38#endif /* GOTO_PROGRAMS_GOTO_TERMINATION_H_ */
goto_functionst
Definition goto_functions.h:56
namespacet
Definition namespace.h:10
optionst
Definition options.h:11
goto_functions.h
goto_termination
void goto_termination(goto_functionst &goto_functions, optionst &options, const namespacet &ns)
Reduce non-termination to a reachability safety property.
Definition goto_termination.cpp:721