49 std::size_t function_calls;
76 else if(i_it->is_assume())
86 else if(i_it->is_goto())
96 else if(i_it->is_assign())
111 if(unchanged_lhs && unchanged_rhs)
112 unmodified.assigns++;
114 simplified.assigns++;
116 else if(i_it->is_function_call())
129 unmodified.function_calls++;
131 simplified.function_calls++;
139 m.
status() <<
"Simplified: " 140 <<
" assert: " << simplified.asserts
141 <<
", assume: " << simplified.assumes
142 <<
", goto: " << simplified.gotos
143 <<
", assigns: " << simplified.assigns
144 <<
", function calls: " << simplified.function_calls
147 <<
" assert: " << unmodified.asserts
148 <<
", assume: " << unmodified.assumes
149 <<
", goto: " << unmodified.gotos
150 <<
", assigns: " << unmodified.assigns
151 <<
", function calls: " << unmodified.function_calls
mstreamt & progress() const
symbol_tablet symbol_table
Symbol table.
virtual std::unique_ptr< statet > abstract_state_before(locationt l) const =0
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
const code_assignt & to_code_assign(const codet &code)
bool write_goto_binary(std::ostream &out, const goto_modelt &goto_model, int version)
Writes a goto program to disc.
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
bool get_bool_option(const std::string &option) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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.
codet representation of a function call statement.
void restore_returns(goto_modelt &goto_model)
restores return statements
Class that provides messages with a built-in verbosity 'level'.
std::vector< exprt > operandst
mstreamt & status() const
The basic interface of an abstract interpreter.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)
goto_functionst goto_functions
GOTO functions.
A codet representing an assignment in the program.
const code_function_callt & to_code_function_call(const codet &code)