|
CBMC
|
#include "static_simplifier.h"#include <util/message.h>#include <util/options.h>#include <goto-programs/goto_model.h>#include <goto-programs/remove_returns.h>#include <goto-programs/remove_skip.h>#include <goto-programs/remove_unreachable.h>#include <goto-programs/write_goto_binary.h>#include <analyses/ai.h>
Include dependency graph for static_simplifier.cpp:Go to the source code of this file.
Functions | |
| bool | static_simplifier (goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out) |
| Simplifies the program using the information in the abstract domain. More... | |
| bool static_simplifier | ( | goto_modelt & | goto_model, |
| const ai_baset & | ai, | ||
| const optionst & | options, | ||
| message_handlert & | message_handler, | ||
| std::ostream & | out | ||
| ) |
Simplifies the program using the information in the abstract domain.
| goto_model | the program analyzed |
| ai | the abstract interpreter after it has been run to fix point |
| options | the parsed user options |
| message_handler | the system message handler |
| out | output stream for the simplified program |
Definition at line 29 of file static_simplifier.cpp.