Skip to content

Commit afe9f5f

Browse files
smowtonpeterschrammel
smowton
authored and
peterschrammel
committed
Make _start optional
Some analyses (such as the security scanner) don't need it, and can tackle problems whose natural _start would be huge and expensive to generate. Thus, make it optional at the frontend.
1 parent da72f88 commit afe9f5f

16 files changed

+53
-24
lines changed

‎src/ansi-c/ansi_c_language.cpp

+8-3
Original file line numberDiff line numberDiff line change
@@ -194,10 +194,15 @@ Function: ansi_c_languaget::final
194194
195195
\*******************************************************************/
196196

197-
bool ansi_c_languaget::final(symbol_tablet &symbol_table)
197+
bool ansi_c_languaget::final(
198+
symbol_tablet &symbol_table,
199+
bool generate_start_function)
198200
{
199-
if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
200-
return true;
201+
if(generate_start_function)
202+
{
203+
if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
204+
return true;
205+
}
201206

202207
return false;
203208
}

‎src/ansi-c/ansi_c_language.h

+2-1
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,8 @@ class ansi_c_languaget:public languaget
3535
const std::string &module) override;
3636

3737
bool final(
38-
symbol_tablet &symbol_table) override;
38+
symbol_tablet &symbol_table,
39+
bool generate_start_function) override;
3940

4041
void show_parse(std::ostream &out) override;
4142

‎src/cpp/cpp_language.cpp

+8-3
Original file line numberDiff line numberDiff line change
@@ -201,10 +201,15 @@ Function: cpp_languaget::final
201201
202202
\*******************************************************************/
203203

204-
bool cpp_languaget::final(symbol_tablet &symbol_table)
204+
bool cpp_languaget::final(
205+
symbol_tablet &symbol_table,
206+
bool generate_start_function)
205207
{
206-
if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
207-
return true;
208+
if(generate_start_function)
209+
{
210+
if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
211+
return true;
212+
}
208213

209214
return false;
210215
}

‎src/cpp/cpp_language.h

+2-1
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,8 @@ class cpp_languaget:public languaget
4141
class replace_symbolt &replace_symbol) const;
4242

4343
bool final(
44-
symbol_tablet &symbol_table) override;
44+
symbol_tablet &symbol_table,
45+
bool generate_start_function) override;
4546

4647
void show_parse(std::ostream &out) override;
4748

‎src/goto-programs/get_goto_model.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -114,7 +114,7 @@ bool get_goto_modelt::operator()(const std::vector<std::string> &files)
114114

115115
if(binaries.empty())
116116
{
117-
if(language_files.final(symbol_table))
117+
if(language_files.final(symbol_table, generate_start_function))
118118
{
119119
error() << "CONVERSION ERROR" << eom;
120120
return true;

‎src/goto-programs/get_goto_model.h

+2
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,9 @@ Author: Daniel Kroening, [email protected]
1616
class get_goto_modelt:public goto_modelt, public messaget
1717
{
1818
public:
19+
get_goto_modelt() : generate_start_function(true) {}
1920
bool operator()(const std::vector<std::string> &);
21+
bool generate_start_function;
2022
};
2123

2224
#endif // CPROVER_GOTO_PROGRAMS_GET_GOTO_MODEL_H

‎src/java_bytecode/java_bytecode_language.cpp

+5-1
Original file line numberDiff line numberDiff line change
@@ -744,13 +744,17 @@ Function: java_bytecode_languaget::final
744744
745745
\*******************************************************************/
746746

747-
bool java_bytecode_languaget::final(symbol_tablet &symbol_table)
747+
bool java_bytecode_languaget::final(
748+
symbol_tablet &symbol_table,
749+
bool generate_start_function)
748750
{
749751
/*
750752
if(c_final(symbol_table, message_handler)) return true;
751753
*/
752754
java_internal_additions(symbol_table);
753755

756+
if(!generate_start_function)
757+
return false;
754758

755759
main_function_resultt res=
756760
get_main_symbol(symbol_table, main_class, get_message_handler());

‎src/java_bytecode/java_bytecode_language.h

+2-1
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,8 @@ class java_bytecode_languaget:public languaget
4949
const std::string &module) override;
5050

5151
bool final(
52-
symbol_tablet &context) override;
52+
symbol_tablet &context,
53+
bool generate_start_function) override;
5354

5455
void show_parse(std::ostream &out) override;
5556

‎src/jsil/jsil_language.cpp

+10-5
Original file line numberDiff line numberDiff line change
@@ -165,12 +165,17 @@ Function: jsil_languaget::final
165165
166166
\*******************************************************************/
167167

168-
bool jsil_languaget::final(symbol_tablet &symbol_table)
168+
bool jsil_languaget::final(
169+
symbol_tablet &symbol_table,
170+
bool generate_start_function)
169171
{
170-
if(jsil_entry_point(
171-
symbol_table,
172-
get_message_handler()))
173-
return true;
172+
if(generate_start_function)
173+
{
174+
if(jsil_entry_point(
175+
symbol_table,
176+
get_message_handler()))
177+
return true;
178+
}
174179

175180
return false;
176181
}

‎src/jsil/jsil_language.h

+2-1
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,8 @@ class jsil_languaget:public languaget
3030
const std::string &module);
3131

3232
virtual bool final(
33-
symbol_tablet &context);
33+
symbol_tablet &context,
34+
bool generate_start_function);
3435

3536
virtual void show_parse(std::ostream &out);
3637

‎src/langapi/language_ui.cpp

+3-2
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,8 @@ language_uit::language_uit(
3434
const cmdlinet &__cmdline,
3535
ui_message_handlert &_ui_message_handler):
3636
ui_message_handler(_ui_message_handler),
37-
_cmdline(__cmdline)
37+
_cmdline(__cmdline),
38+
generate_start_function(true)
3839
{
3940
set_message_handler(ui_message_handler);
4041
}
@@ -183,7 +184,7 @@ bool language_uit::final()
183184
{
184185
language_files.set_message_handler(*message_handler);
185186

186-
if(language_files.final(symbol_table))
187+
if(language_files.final(symbol_table, generate_start_function))
187188
{
188189
if(get_ui()==ui_message_handlert::PLAIN)
189190
std::cerr << "CONVERSION ERROR" << std::endl;

‎src/langapi/language_ui.h

+1
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,7 @@ class language_uit:public messaget
5252

5353
protected:
5454
const cmdlinet &_cmdline;
55+
bool generate_start_function;
5556
};
5657

5758
#endif // CPROVER_LANGAPI_LANGUAGE_UI_H

‎src/util/language.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ Function: languaget::final
2121
2222
\*******************************************************************/
2323

24-
bool languaget::final(symbol_tablet &symbol_table)
24+
bool languaget::final(symbol_tablet &symbol_table, bool generate_start_function)
2525
{
2626
return false;
2727
}

‎src/util/language.h

+2-1
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,8 @@ class languaget:public messaget
6161
// final adjustments, e.g., initialization and call to main()
6262

6363
virtual bool final(
64-
symbol_tablet &symbol_table);
64+
symbol_tablet &symbol_table,
65+
bool generate_start_function);
6566

6667
// type check interfaces of currently parsed file
6768

‎src/util/language_file.cpp

+3-2
Original file line numberDiff line numberDiff line change
@@ -235,15 +235,16 @@ Function: language_filest::final
235235
\*******************************************************************/
236236

237237
bool language_filest::final(
238-
symbol_tablet &symbol_table)
238+
symbol_tablet &symbol_table,
239+
bool generate_start_function)
239240
{
240241
std::set<std::string> languages;
241242

242243
for(file_mapt::iterator it=file_map.begin();
243244
it!=file_map.end(); it++)
244245
{
245246
if(languages.insert(it->second.language->id()).second)
246-
if(it->second.language->final(symbol_table))
247+
if(it->second.language->final(symbol_table, generate_start_function))
247248
return true;
248249
}
249250

‎src/util/language_file.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -81,7 +81,7 @@ class language_filest:public messaget
8181

8282
bool typecheck(symbol_tablet &symbol_table);
8383

84-
bool final(symbol_tablet &symbol_table);
84+
bool final(symbol_tablet &symbol_table, bool generate_start_function);
8585

8686
bool interfaces(symbol_tablet &symbol_table);
8787

0 commit comments

Comments
 (0)