Go to the documentation of this file.
49 std::size_t function_calls;
68 exprt cond = i_it->get_condition();
77 i_it->set_condition(cond);
80 else if(i_it->is_assume())
82 exprt cond = i_it->get_condition();
91 i_it->set_condition(cond);
94 else if(i_it->is_goto())
96 exprt cond = i_it->get_condition();
105 i_it->set_condition(cond);
108 else if(i_it->is_assign())
110 auto assign = i_it->get_assign();
123 if(unchanged_lhs && unchanged_rhs)
124 unmodified.assigns++;
127 simplified.assigns++;
128 i_it->set_assign(assign);
131 else if(i_it->is_function_call())
133 auto fcall = i_it->get_function_call();
144 unmodified.function_calls++;
147 simplified.function_calls++;
148 i_it->set_function_call(fcall);
157 m.
status() <<
"Simplified: "
158 <<
" assert: " << simplified.asserts
159 <<
", assume: " << simplified.assumes
160 <<
", goto: " << simplified.gotos
161 <<
", assigns: " << simplified.assigns
162 <<
", function calls: " << simplified.function_calls
165 <<
" assert: " << unmodified.asserts
166 <<
", assume: " << unmodified.assumes
167 <<
", goto: " << unmodified.gotos
168 <<
", assigns: " << unmodified.assigns
169 <<
", function calls: " << unmodified.function_calls
Class that provides messages with a built-in verbosity 'level'.
#define Forall_goto_program_instructions(it, program)
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.
mstreamt & status() const
bool write_goto_binary(std::ostream &out, const symbol_tablet &symbol_table, const goto_functionst &goto_functions, irep_serializationt &irepconverter)
Writes a goto program to disc, using goto binary format.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Base class for all expressions.
virtual cstate_ptrt abstract_state_before(locationt l) const
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
void remove_unreachable(goto_programt &goto_program)
remove unreachable code
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::vector< exprt > operandst
#define Forall_goto_functions(it, functions)
Replace function returns by assignments to global variables.
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
goto_functionst goto_functions
GOTO functions.
bool get_bool_option(const std::string &option) const
This is the basic interface of the abstract interpreter with default implementations of the core func...
mstreamt & progress() const
symbol_tablet symbol_table
Symbol table.
void restore_returns(goto_modelt &goto_model)
restores return statements