cprover
|
#include <remove_calls_no_body.h>
Public Member Functions | |
void | operator() (goto_programt &goto_program, const goto_functionst &goto_functions) |
Remove calls to functions without a body and replace them with evaluations of the arguments of the call and a nondet assignment to the variable taking the return value. More... | |
void | operator() (goto_functionst &goto_functions) |
Remove calls to functions without a body and replace them with evaluations of the arguments of the call and a nondet assignment to the variable taking the return value. More... | |
Protected Member Functions | |
bool | is_opaque_function_call (const goto_programt::const_targett target, const goto_functionst &goto_functions) |
Check if instruction is a call to an opaque function through an ordinary (non-function pointer) call. More... | |
void | remove_call_no_body (goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments) |
Remove a single call. More... | |
Definition at line 19 of file remove_calls_no_body.h.
|
protected |
Check if instruction is a call to an opaque function through an ordinary (non-function pointer) call.
target | iterator pointing to the instruction to check |
goto_functions | all goto function to look up call target |
Definition at line 70 of file remove_calls_no_body.cpp.
References code_function_callt::function(), goto_functionst::function_map, symbol_exprt::get_identifier(), irept::id(), to_code_function_call(), and to_symbol_expr().
Referenced by operator()().
void remove_calls_no_bodyt::operator() | ( | goto_programt & | goto_program, |
const goto_functionst & | goto_functions | ||
) |
Remove calls to functions without a body and replace them with evaluations of the arguments of the call and a nondet assignment to the variable taking the return value.
goto_program | goto program to operate on |
goto_functions | all goto functions; for looking up functions which the goto program may call |
Definition at line 104 of file remove_calls_no_body.cpp.
References code_function_callt::arguments(), goto_program, goto_programt::instructions, is_opaque_function_call(), code_function_callt::lhs(), remove_call_no_body(), and to_code_function_call().
void remove_calls_no_bodyt::operator() | ( | goto_functionst & | goto_functions | ) |
Remove calls to functions without a body and replace them with evaluations of the arguments of the call and a nondet assignment to the variable taking the return value.
goto_functions | goto functions to operate on |
Definition at line 125 of file remove_calls_no_body.cpp.
References Forall_goto_functions.
|
protected |
Remove a single call.
goto_program | goto program to modify |
target | iterator pointing to the call |
lhs | lhs of the call to which the return value is assigned |
arguments | arguments of the call |
Definition at line 23 of file remove_calls_no_body.cpp.
References goto_programt::add_instruction(), ASSIGN, goto_programt::destructive_insert(), goto_programt::empty(), goto_program, irept::is_not_nil(), LOCATION, PRECONDITION, typet::source_location(), and exprt::type().
Referenced by operator()().