File tree 7 files changed +24
-5
lines changed 7 files changed +24
-5
lines changed Original file line number Diff line number Diff line change @@ -29,7 +29,7 @@ bool internal_functions_filtert::operator()(
29
29
if (function.name == INITIALIZE_FUNCTION)
30
30
return false ;
31
31
32
- if (goto_function .is_hidden ())
32
+ if (to_code_type (function. type ) .is_hidden ())
33
33
return false ;
34
34
35
35
// ignore Java built-ins (synthetic functions)
Original file line number Diff line number Diff line change @@ -216,7 +216,10 @@ void goto_convert_functionst::convert_function(
216
216
f.body .update ();
217
217
218
218
if (hide (f.body ))
219
+ {
219
220
f.make_hidden ();
221
+ to_code_type (symbol_table.get_writeable_ref (identifier).type ).make_hidden ();
222
+ }
220
223
221
224
lifetime = parent_lifetime;
222
225
}
Original file line number Diff line number Diff line change @@ -253,7 +253,7 @@ void goto_inlinet::insert_function_body(
253
253
end.type =LOCATION;
254
254
255
255
// make sure the inlined function does not introduce hiding
256
- if (goto_function .is_hidden ())
256
+ if (to_code_type (ns. lookup (identifier). type ) .is_hidden ())
257
257
{
258
258
for (auto &instruction : body.instructions )
259
259
instruction.labels .remove (CPROVER_PREFIX " HIDE" );
Original file line number Diff line number Diff line change @@ -160,7 +160,10 @@ static bool read_bin_goto_object(
160
160
f.body .update ();
161
161
162
162
if (hidden)
163
+ {
163
164
f.make_hidden ();
165
+ to_code_type (symbol_table.get_writeable_ref (fname).type ).make_hidden ();
166
+ }
164
167
}
165
168
166
169
functions.compute_location_numbers ();
Original file line number Diff line number Diff line change @@ -274,7 +274,9 @@ void goto_symext::symex_function_call_code(
274
274
a = state.rename (std::move (a), ns);
275
275
276
276
// we hide the call if the caller and callee are both hidden
277
- const bool hidden = state.top ().hidden_function && goto_function.is_hidden ();
277
+ const bool callee_is_hidden =
278
+ to_code_type (ns.lookup (identifier).type ).is_hidden ();
279
+ const bool hidden = state.top ().hidden_function && callee_is_hidden;
278
280
279
281
// record the call
280
282
target.function_call (
@@ -313,7 +315,7 @@ void goto_symext::symex_function_call_code(
313
315
frame.end_of_function =--goto_function.body .instructions .end ();
314
316
frame.return_value =call.lhs ();
315
317
frame.function_identifier =identifier;
316
- frame.hidden_function =goto_function. is_hidden () ;
318
+ frame.hidden_function = callee_is_hidden ;
317
319
318
320
const framet &p_frame = state.previous_frame ();
319
321
for (const auto &pair : p_frame.loop_iterations )
Original file line number Diff line number Diff line change @@ -325,7 +325,8 @@ std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
325
325
std::prev (start_function->body .instructions .end ());
326
326
state->top ().end_of_function = limit;
327
327
state->top ().calling_location .pc = state->top ().end_of_function ;
328
- state->top ().hidden_function = start_function->is_hidden ();
328
+ state->top ().hidden_function =
329
+ to_code_type (ns.lookup (entry_point_id).type ).is_hidden ();
329
330
330
331
state->symex_target = ⌖
331
332
Original file line number Diff line number Diff line change @@ -896,6 +896,16 @@ class code_typet:public typet
896
896
set (ID_C_inlined, value);
897
897
}
898
898
899
+ bool is_hidden () const
900
+ {
901
+ return get_bool (ID_C_hide);
902
+ }
903
+
904
+ void make_hidden ()
905
+ {
906
+ set (ID_C_hide, true );
907
+ }
908
+
899
909
const irep_idt &get_access () const
900
910
{
901
911
return get (ID_access);
You can’t perform that action at this time.
0 commit comments