Skip to content

Commit a9cd423

Browse files
committed
Store "is hidden" attribute of goto functions in the symbol table
There should only be a single place to hold type information, including attributes, to ensure consistency. Future changes will remove the "type" member of goto_functiont, making the type information stored in the symbol table the single, authoritative source of information. With this commit the information will remain available in both places, but all read accesses only use the information in the symbol table.
1 parent 95e15fd commit a9cd423

File tree

8 files changed

+25
-5
lines changed

8 files changed

+25
-5
lines changed

src/goto-instrument/cover_filter.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ bool internal_functions_filtert::operator()(
2929
if(function.name == INITIALIZE_FUNCTION)
3030
return false;
3131

32-
if(goto_function.is_hidden())
32+
if(to_code_type(function.type).is_hidden())
3333
return false;
3434

3535
// ignore Java built-ins (synthetic functions)

src/goto-programs/goto_convert_functions.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -216,7 +216,10 @@ void goto_convert_functionst::convert_function(
216216
f.body.update();
217217

218218
if(hide(f.body))
219+
{
219220
f.make_hidden();
221+
to_code_type(symbol_table.get_writeable_ref(identifier).type).make_hidden();
222+
}
220223

221224
lifetime = parent_lifetime;
222225
}

src/goto-programs/goto_inline_class.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -253,7 +253,7 @@ void goto_inlinet::insert_function_body(
253253
end.type=LOCATION;
254254

255255
// 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())
257257
{
258258
for(auto &instruction : body.instructions)
259259
instruction.labels.remove(CPROVER_PREFIX "HIDE");

src/goto-programs/read_bin_goto_object.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -160,7 +160,10 @@ static bool read_bin_goto_object(
160160
f.body.update();
161161

162162
if(hidden)
163+
{
163164
f.make_hidden();
165+
to_code_type(symbol_table.get_writeable_ref(fname).type).make_hidden();
166+
}
164167
}
165168

166169
functions.compute_location_numbers();

src/goto-symex/symex_function_call.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -274,7 +274,9 @@ void goto_symext::symex_function_call_code(
274274
a = state.rename(std::move(a), ns);
275275

276276
// 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;
278280

279281
// record the call
280282
target.function_call(
@@ -313,7 +315,7 @@ void goto_symext::symex_function_call_code(
313315
frame.end_of_function=--goto_function.body.instructions.end();
314316
frame.return_value=call.lhs();
315317
frame.function_identifier=identifier;
316-
frame.hidden_function=goto_function.is_hidden();
318+
frame.hidden_function = callee_is_hidden;
317319

318320
const framet &p_frame = state.previous_frame();
319321
for(const auto &pair : p_frame.loop_iterations)

src/goto-symex/symex_main.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -325,7 +325,8 @@ std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
325325
std::prev(start_function->body.instructions.end());
326326
state->top().end_of_function = limit;
327327
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();
329330

330331
state->symex_target = &target;
331332

src/util/std_types.h

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -896,6 +896,16 @@ class code_typet:public typet
896896
set(ID_C_inlined, value);
897897
}
898898

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+
899909
const irep_idt &get_access() const
900910
{
901911
return get(ID_access);

unit/goto-instrument/cover/cover_only.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ symbolt create_new_symbol(const irep_idt &name, const irep_idt &file_name)
2222
source_locationt location;
2323
location.set_file(file_name);
2424
symbol.location = location;
25+
symbol.type = code_typet{{}, empty_typet{}};
2526

2627
return symbol;
2728
}

0 commit comments

Comments
 (0)