cprover
Loading...
Searching...
No Matches
remove_calls_no_body.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Remove calls to functions without a body
4
5Author: Daniel Poetzl
6
7\*******************************************************************/
8
11
13
14#include <util/invariant.h>
15#include <util/std_code.h>
16
17#include "goto_functions.h"
18
25 goto_programt &goto_program,
27 const exprt &lhs,
28 const exprt::operandst &arguments)
29{
30 PRECONDITION(target->is_function_call());
31 PRECONDITION(!goto_program.empty());
32
33 goto_programt tmp;
34
35 // evaluate function arguments -- they might have
36 // pointer dereferencing or the like
37 for(const exprt &argument : arguments)
38 {
40 code_expressiont(argument), target->source_location()));
41 }
42
43 // return value
44 if(lhs.is_not_nil())
45 {
46 side_effect_expr_nondett rhs(lhs.type(), target->source_location());
47
48 code_assignt code(lhs, rhs);
49 code.add_source_location() = target->source_location();
50
52 }
53
54 // kill call
55 *target = goto_programt::make_location(target->source_location());
56 target++;
57
58 goto_program.destructive_insert(target, tmp);
59}
60
67 const goto_functionst &goto_functions)
68{
69 if(!target->is_function_call())
70 return false;
71
72 const exprt &f = target->call_function();
73
74 if(f.id() != ID_symbol)
75 return false;
76
77 const symbol_exprt &se = to_symbol_expr(f);
78 const irep_idt id = se.get_identifier();
79
80 goto_functionst::function_mapt::const_iterator f_it =
81 goto_functions.function_map.find(id);
82
83 if(f_it != goto_functions.function_map.end())
84 {
85 return !f_it->second.body_available();
86 }
87
88 return false;
89}
90
98operator()(goto_programt &goto_program, const goto_functionst &goto_functions)
99{
100 for(goto_programt::targett it = goto_program.instructions.begin();
101 it != goto_program.instructions.end();) // no it++
102 {
103 if(is_opaque_function_call(it, goto_functions))
104 {
106 goto_program, it, it->call_lhs(), it->call_arguments());
107 }
108 else
109 {
110 it++;
111 }
112 }
113}
114
120{
121 for(auto &gf_entry : goto_functions.function_map)
122 {
123 (*this)(gf_entry.second.body, goto_functions);
124 }
125}
A codet representing an assignment in the program.
codet representation of an expression statement.
Definition: std_code.h:1394
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:706
instructionst::iterator targett
Definition: goto_program.h:592
instructionst::const_iterator const_targett
Definition: goto_program.h:593
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_location(const source_locationt &l)
Definition: goto_program.h:890
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:715
bool empty() const
Is the program empty?
Definition: goto_program.h:788
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:942
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
void remove_call_no_body(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
Remove a single call.
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.
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 ca...
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
const source_locationt & source_location() const
Definition: type.h:74
Goto Programs with Functions.
Remove calls to functions without a body.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189