@@ -22,8 +22,8 @@ Date: June 2003
22
22
23
23
goto_convert_functionst::goto_convert_functionst (
24
24
symbol_table_baset &_symbol_table,
25
- message_handlert &_message_handler):
26
- goto_convertt(_symbol_table, _message_handler)
25
+ message_handlert &_message_handler)
26
+ : goto_convertt(_symbol_table, _message_handler)
27
27
{
28
28
}
29
29
@@ -59,8 +59,8 @@ void goto_convert_functionst::goto_convert(goto_functionst &functions)
59
59
60
60
functions.compute_location_numbers ();
61
61
62
- // this removes the parse tree of the bodies from memory
63
- #if 0
62
+ // this removes the parse tree of the bodies from memory
63
+ #if 0
64
64
for(const auto &symbol_pair, symbol_table.symbols)
65
65
{
66
66
if(!symbol_pair.second.is_type &&
@@ -70,7 +70,7 @@ void goto_convert_functionst::goto_convert(goto_functionst &functions)
70
70
symbol_pair.second.value=codet();
71
71
}
72
72
}
73
- #endif
73
+ #endif
74
74
}
75
75
76
76
bool goto_convert_functionst::hide (const goto_programt &goto_program)
@@ -89,7 +89,7 @@ void goto_convert_functionst::add_return(
89
89
goto_functionst::goto_functiont &f,
90
90
const source_locationt &source_location)
91
91
{
92
- #if 0
92
+ #if 0
93
93
if(!f.body.instructions.empty() &&
94
94
f.body.instructions.back().is_return())
95
95
return; // not needed, we have one already
@@ -99,12 +99,11 @@ void goto_convert_functionst::add_return(
99
99
f.body.instructions.back().is_goto() &&
100
100
f.body.instructions.back().guard.is_true())
101
101
return;
102
- #else
102
+ #else
103
103
104
104
if (!f.body .instructions .empty ())
105
105
{
106
- goto_programt::const_targett last_instruction=
107
- f.body .instructions .end ();
106
+ goto_programt::const_targett last_instruction = f.body .instructions .end ();
108
107
last_instruction--;
109
108
110
109
while (true )
@@ -122,16 +121,17 @@ void goto_convert_functionst::add_return(
122
121
return ;
123
122
124
123
// advance if it's a 'dead' without branch target
125
- if (last_instruction->is_dead () &&
126
- last_instruction!=f.body .instructions .begin () &&
127
- !last_instruction->is_target ())
124
+ if (
125
+ last_instruction->is_dead () &&
126
+ last_instruction != f.body .instructions .begin () &&
127
+ !last_instruction->is_target ())
128
128
last_instruction--;
129
129
else
130
130
break ; // give up
131
131
}
132
132
}
133
133
134
- #endif
134
+ #endif
135
135
136
136
side_effect_expr_nondett rhs (f.type .return_type (), source_location);
137
137
@@ -143,22 +143,23 @@ void goto_convert_functionst::convert_function(
143
143
const irep_idt &identifier,
144
144
goto_functionst::goto_functiont &f)
145
145
{
146
- const symbolt &symbol= ns.lookup (identifier);
146
+ const symbolt &symbol = ns.lookup (identifier);
147
147
const irep_idt mode = symbol.mode ;
148
148
149
149
if (f.body_available ())
150
150
return ; // already converted
151
151
152
152
// make tmp variables local to function
153
- tmp_symbol_prefix= id2string (symbol.name )+ " ::$tmp" ;
153
+ tmp_symbol_prefix = id2string (symbol.name ) + " ::$tmp" ;
154
154
155
155
// store the parameter identifiers in the goto functions
156
156
const code_typet &code_type = to_code_type (symbol.type );
157
157
f.type = code_type;
158
158
f.set_parameter_identifiers (code_type);
159
159
160
- if (symbol.value .is_nil () ||
161
- symbol.is_compiled ()) /* goto_inline may have removed the body */
160
+ if (
161
+ symbol.value .is_nil () ||
162
+ symbol.is_compiled ()) /* goto_inline may have removed the body */
162
163
return ;
163
164
164
165
// we have a body, make sure all parameter names are valid
@@ -174,25 +175,24 @@ void goto_convert_functionst::convert_function(
174
175
lifetime = identifier == INITIALIZE_FUNCTION ? lifetimet::STATIC_GLOBAL
175
176
: lifetimet::AUTOMATIC_LOCAL;
176
177
177
- const codet &code= to_code (symbol.value );
178
+ const codet &code = to_code (symbol.value );
178
179
179
180
source_locationt end_location;
180
181
181
- if (code.get_statement ()== ID_block)
182
- end_location= to_code_block (code).end_location ();
182
+ if (code.get_statement () == ID_block)
183
+ end_location = to_code_block (code).end_location ();
183
184
else
184
185
end_location.make_nil ();
185
186
186
187
goto_programt tmp_end_function;
187
188
goto_programt::targett end_function =
188
189
tmp_end_function.add (goto_programt::make_end_function (end_location));
189
190
190
- targets= targetst ();
191
+ targets = targetst ();
191
192
targets.set_return (end_function);
192
- targets.has_return_value =
193
- f.type .return_type ().id ()!=ID_empty &&
194
- f.type .return_type ().id ()!=ID_constructor &&
195
- f.type .return_type ().id ()!=ID_destructor;
193
+ targets.has_return_value = f.type .return_type ().id () != ID_empty &&
194
+ f.type .return_type ().id () != ID_constructor &&
195
+ f.type .return_type ().id () != ID_destructor;
196
196
197
197
goto_convert_rec (code, f.body , mode);
198
198
@@ -201,12 +201,13 @@ void goto_convert_functionst::convert_function(
201
201
add_return (f, end_location);
202
202
203
203
// handle SV-COMP's __VERIFIER_atomic_
204
- if (!f.body .instructions .empty () &&
205
- has_prefix (id2string (identifier), " __VERIFIER_atomic_" ))
204
+ if (
205
+ !f.body .instructions .empty () &&
206
+ has_prefix (id2string (identifier), " __VERIFIER_atomic_" ))
206
207
{
207
208
goto_programt::instructiont a_begin;
208
209
a_begin = goto_programt::make_atomic_begin ();
209
- a_begin.source_location = f.body .instructions .front ().source_location ;
210
+ a_begin.source_location = f.body .instructions .front ().source_location ;
210
211
f.body .insert_before_swap (f.body .instructions .begin (), a_begin);
211
212
212
213
goto_programt::targett a_end =
@@ -233,9 +234,7 @@ void goto_convert_functionst::convert_function(
233
234
lifetime = parent_lifetime;
234
235
}
235
236
236
- void goto_convert (
237
- goto_modelt &goto_model,
238
- message_handlert &message_handler)
237
+ void goto_convert (goto_modelt &goto_model, message_handlert &message_handler)
239
238
{
240
239
symbol_table_buildert symbol_table_builder =
241
240
symbol_table_buildert::wrap (goto_model.symbol_table );
0 commit comments