ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
goto_loop_simplify.h
Go to the documentation of this file.
1#ifndef GOTO_PROGRAMS_GOTO_LOOP_SIMPLIFY_H_
2#define GOTO_PROGRAMS_GOTO_LOOP_SIMPLIFY_H_
3
4#include <goto-programs/goto_functions.h>
5#include <util/config/options.h>
6
34void goto_loop_simplify(
35 goto_functionst &goto_functions,
36 const optionst &options);
37
38#endif
goto_functionst
Definition goto_functions.h:56
optionst
Definition options.h:11
goto_functions.h
goto_loop_simplify
void goto_loop_simplify(goto_functionst &goto_functions, const optionst &options)
Detect and remove no-op loops at goto-program level, before symex.
Definition goto_loop_simplify.cpp:780