ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
non_termination.h
Go to the documentation of this file.
1#ifndef ESBMC_NON_TERMINATION_H
2#define ESBMC_NON_TERMINATION_H
3
4#include <goto-programs/goto_functions.h>
5#include <util/symtab/namespace.h>
6#include <util/config/options.h>
7#include <util/base/threeval.h>
8
40tvt try_prove_non_termination_by_recurrent_set(
41 goto_functionst &goto_functions,
42 optionst &options,
43 const namespacet &ns);
44
45#endif /* ESBMC_NON_TERMINATION_H */
goto_functionst
Definition goto_functions.h:56
namespacet
Definition namespace.h:10
optionst
Definition options.h:11
tvt
Definition threeval.h:10
goto_functions.h
try_prove_non_termination_by_recurrent_set
tvt try_prove_non_termination_by_recurrent_set(goto_functionst &goto_functions, optionst &options, const namespacet &ns)
Period-1 fixpoint non-termination check, restricted to the eca- rers2012 main-loop shape.
Definition non_termination.cpp:618