Skip to content

Commit 4a2de0d

Browse files
Make filter_goto_model remove file local symbols
Since we want goto_harness to print out as little as possible to be useful this is helpful, and this also lets us avoid bugs with duplicate definitions (e.g. a static variable that’s now in the produced harness.c – and thus a *different* static variable!). Also marks non-file-local globals as extern so we avoid double definitions.
1 parent 4ca4239 commit 4a2de0d

File tree

1 file changed

+28
-5
lines changed

1 file changed

+28
-5
lines changed

src/goto-harness/goto_harness_parse_options.cpp

Lines changed: 28 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -51,12 +51,35 @@ static void filter_goto_model(
5151
goto_modelt &goto_model_with_harness,
5252
const std::unordered_set<irep_idt> &goto_model_without_harness_symbols)
5353
{
54-
for(auto &symbol : goto_model_with_harness.get_symbol_table())
54+
for(auto const &symbol_id : goto_model_without_harness_symbols)
5555
{
56-
if(
57-
goto_model_without_harness_symbols.count(symbol.first) == 1 &&
58-
symbol.second.is_function())
59-
goto_model_with_harness.unload(symbol.first);
56+
auto &symbol =
57+
goto_model_with_harness.symbol_table.get_writeable_ref(symbol_id);
58+
if(symbol.is_function())
59+
{
60+
// We don’t want bodies of functions that already existed in the
61+
// symbol table (i.e. not generated by us)
62+
goto_model_with_harness.unload(symbol_id);
63+
if(symbol.is_file_local)
64+
{
65+
goto_model_with_harness.symbol_table.remove(symbol_id);
66+
}
67+
}
68+
else if(!symbol.is_type && symbol.is_file_local)
69+
{
70+
// We don’t want file local symbols from an existing goto model
71+
// except types / typedefs, which also apparently get marked
72+
// file local sometimes.
73+
goto_model_with_harness.symbol_table.remove(symbol_id);
74+
}
75+
else if(!symbol.is_type && symbol.is_static_lifetime)
76+
{
77+
// if it has static lifetime and is *not* a type it is a global variable
78+
// We keep around other global variables in case we want to initialise
79+
// them, but mark them as extern so we don't duplicate their definitions
80+
symbol.value = nil_exprt{};
81+
symbol.is_extern = true;
82+
}
6083
}
6184
}
6285

0 commit comments

Comments
 (0)