Skip to content

Commit c003aa2

Browse files
tautschnigkroening
authored andcommitted
Read "is inlined" attribute of goto functions from 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. The "is inlined" information should already be consistent/redundant. This commit makes all read accesses use the information stored in the symbol table, and also uses a modern API for doing so.
1 parent 0e16cbb commit c003aa2

File tree

11 files changed

+35
-25
lines changed

11 files changed

+35
-25
lines changed

src/ansi-c/ansi_c_declaration.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -150,7 +150,7 @@ void ansi_c_declarationt::to_symbol(
150150
symbol.is_file_local=get_is_static();
151151

152152
if(get_is_inline())
153-
symbol.type.set(ID_C_inlined, true);
153+
to_code_type(symbol.type).set_inlined(true);
154154

155155
if(
156156
config.ansi_c.mode == configt::ansi_ct::flavourt::GCC ||

src/ansi-c/c_typecheck_base.cpp

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -309,10 +309,6 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
309309

310310
if(final_new.id()==ID_code)
311311
{
312-
bool inlined=
313-
(new_symbol.type.get_bool(ID_C_inlined) ||
314-
old_symbol.type.get_bool(ID_C_inlined));
315-
316312
if(final_old.id()!=ID_code)
317313
{
318314
error().source_location=new_symbol.location;
@@ -327,15 +323,17 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
327323
code_typet &old_ct=to_code_type(old_symbol.type);
328324
code_typet &new_ct=to_code_type(new_symbol.type);
329325

326+
const bool inlined = old_ct.get_inlined() || new_ct.get_inlined();
327+
330328
if(old_ct.has_ellipsis() && !new_ct.has_ellipsis())
331329
old_ct=new_ct;
332330
else if(!old_ct.has_ellipsis() && new_ct.has_ellipsis())
333331
new_ct=old_ct;
334332

335333
if(inlined)
336334
{
337-
old_symbol.type.set(ID_C_inlined, true);
338-
new_symbol.type.set(ID_C_inlined, true);
335+
old_ct.set_inlined(true);
336+
new_ct.set_inlined(true);
339337
}
340338

341339
// do body
@@ -348,7 +346,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
348346
// definition is marked as "extern inline"
349347

350348
if(
351-
old_symbol.type.get_bool(ID_C_inlined) &&
349+
old_ct.get_inlined() &&
352350
(config.ansi_c.mode == configt::ansi_ct::flavourt::GCC ||
353351
config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG ||
354352
config.ansi_c.mode == configt::ansi_ct::flavourt::ARM ||

src/cpp/cpp_declarator_converter.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -462,7 +462,7 @@ symbolt &cpp_declarator_convertert::convert_new_symbol(
462462
symbol.is_macro=true;
463463

464464
if(member_spec.is_inline())
465-
symbol.type.set(ID_C_inlined, true);
465+
to_code_type(symbol.type).set_inlined(true);
466466

467467
if(!symbol.is_type)
468468
{

src/cpp/cpp_typecheck_compound_type.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1293,7 +1293,7 @@ void cpp_typecheckt::typecheck_member_function(
12931293
component.set(ID_prefix, id2string(identifier) + "::");
12941294

12951295
if(value.is_not_nil())
1296-
type.set(ID_C_inlined, true);
1296+
to_code_type(type).set_inlined(true);
12971297

12981298
symbol.name=identifier;
12991299
symbol.base_name=component.get_base_name();

src/goto-analyzer/unreachable_instructions.cpp

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -173,9 +173,12 @@ void unreachable_instructions(
173173

174174
// f_it->first may be a link-time renamed version, use the
175175
// base_name instead; do not list inlined functions
176-
if(called.find(decl.base_name)!=called.end() ||
177-
f_it->second.is_inlined())
176+
if(
177+
called.find(decl.base_name) != called.end() ||
178+
to_code_type(decl.type).get_inlined())
179+
{
178180
unreachable_instructions(goto_program, dead_map);
181+
}
179182
else
180183
all_unreachable(goto_program, dead_map);
181184

@@ -295,10 +298,12 @@ static void list_functions(
295298

296299
// f_it->first may be a link-time renamed version, use the
297300
// base_name instead; do not list inlined functions
298-
if(unreachable ==
299-
(called.find(decl.base_name)!=called.end() ||
300-
f_it->second.is_inlined()))
301+
if(
302+
unreachable == (called.find(decl.base_name) != called.end() ||
303+
to_code_type(decl.type).get_inlined()))
304+
{
301305
continue;
306+
}
302307

303308
source_locationt first_location=decl.location;
304309

src/goto-instrument/aggressive_slicer.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,9 +39,11 @@ void aggressive_slicert::note_functions_to_keep(
3939

4040
void aggressive_slicert::get_all_functions_containing_properties()
4141
{
42+
const namespacet ns(goto_model.symbol_table);
43+
4244
for(const auto &fct : goto_model.goto_functions.function_map)
4345
{
44-
if(!fct.second.is_inlined())
46+
if(!to_code_type(ns.lookup(fct.first).type).get_inlined())
4547
{
4648
for(const auto &ins : fct.second.body.instructions)
4749
if(ins.is_assert())

src/goto-instrument/remove_function.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,8 @@ void remove_function(
3939
<< " in goto program" << messaget::eom;
4040
return;
4141
}
42-
else if(entry->second.is_inlined())
42+
else if(to_code_type(goto_model.symbol_table.lookup_ref(identifier).type)
43+
.get_inlined())
4344
{
4445
message.warning() << "Function " << identifier << " is inlined, "
4546
<< "instantiations will not be removed"

src/goto-programs/goto_inline.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -194,7 +194,7 @@ void goto_partial_inline(
194194
continue;
195195

196196
if(
197-
called_function.is_inlined() ||
197+
to_code_type(ns.lookup(id).type).get_inlined() ||
198198
called_function.body.instructions.size() <= smallfunc_limit)
199199
{
200200
PRECONDITION(i_it->is_function_call());

src/goto-programs/link_goto_model.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,7 @@ static bool link_functions(
104104
{
105105
// just keep the old one in dest
106106
}
107-
else if(in_dest_symbol_table.type.get_bool(ID_C_inlined))
107+
else if(to_code_type(ns.lookup(final_id).type).get_inlined())
108108
{
109109
// ok, we silently ignore
110110
}

src/goto-programs/property_checker.cpp

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -30,12 +30,15 @@ property_checkert::property_checkert(
3030
{
3131
}
3232

33-
void property_checkert::initialize_property_map(
34-
const goto_functionst &goto_functions)
33+
void property_checkert::initialize_property_map(const goto_modelt &goto_model)
3534
{
36-
forall_goto_functions(it, goto_functions)
37-
if(!it->second.is_inlined() ||
38-
it->first==goto_functions.entry_point())
35+
const namespacet ns(goto_model.symbol_table);
36+
37+
forall_goto_functions(it, goto_model.goto_functions)
38+
{
39+
if(
40+
!to_code_type(ns.lookup(it->first).type).get_inlined() ||
41+
it->first == goto_functionst::entry_point())
3942
{
4043
const goto_programt &goto_program=it->second.body;
4144

@@ -53,4 +56,5 @@ void property_checkert::initialize_property_map(
5356
property_status.location=i_it;
5457
}
5558
}
59+
}
5660
}

0 commit comments

Comments
 (0)