Skip to content

Commit 50170f0

Browse files
committed
goto-analyzer --reachable-functions
Provide the complement of --unreachable-functions
1 parent 68bded3 commit 50170f0

File tree

5 files changed

+83
-9
lines changed

5 files changed

+83
-9
lines changed

CHANGELOG

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33

44
* GOTO-INSTRUMENT: New option --list-calls-args
55
* GOTO-INSTRUMENT: New option --print-path-lenghts
6-
* GOTO-ANALYZER: New option --unreachable-functions
6+
* GOTO-ANALYZER: New option --unreachable-functions, --reachable-functions
77

88

99
5.7

src/goto-analyzer/goto_analyzer_parse_options.cpp

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -289,6 +289,30 @@ int goto_analyzer_parse_optionst::doit()
289289
return 0;
290290
}
291291

292+
if(cmdline.isset("reachable-functions"))
293+
{
294+
const std::string json_file=cmdline.get_value("json");
295+
296+
if(json_file.empty())
297+
reachable_functions(goto_model, false, std::cout);
298+
else if(json_file=="-")
299+
reachable_functions(goto_model, true, std::cout);
300+
else
301+
{
302+
std::ofstream ofs(json_file);
303+
if(!ofs)
304+
{
305+
error() << "Failed to open json output `"
306+
<< json_file << "'" << eom;
307+
return 6;
308+
}
309+
310+
reachable_functions(goto_model, true, ofs);
311+
}
312+
313+
return 0;
314+
}
315+
292316
if(cmdline.isset("show-local-may-alias"))
293317
{
294318
namespacet ns(goto_model.symbol_table);
@@ -515,6 +539,8 @@ void goto_analyzer_parse_optionst::help()
515539
" --unreachable-instructions list dead code\n"
516540
// NOLINTNEXTLINE(whitespace/line_length)
517541
" --unreachable-functions list functions unreachable from the entry point\n"
542+
// NOLINTNEXTLINE(whitespace/line_length)
543+
" --reachable-functions list functions reachable from the entry point\n"
518544
" --intervals interval analysis\n"
519545
" --non-null non-null analysis\n"
520546
"\n"

src/goto-analyzer/goto_analyzer_parse_options.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,7 @@ class optionst;
3737
"(show-local-may-alias)" \
3838
"(json):(xml):" \
3939
"(unreachable-instructions)(unreachable-functions)" \
40+
"(reachable-functions)" \
4041
"(intervals)(show-intervals)" \
4142
"(non-null)(show-non-null)"
4243

src/goto-analyzer/unreachable_instructions.cpp

Lines changed: 50 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -223,7 +223,7 @@ void unreachable_instructions(
223223

224224
/*******************************************************************\
225225
226-
Function: output_unreachable_function
226+
Function: json_output_function
227227
228228
Inputs:
229229
@@ -233,7 +233,7 @@ Function: output_unreachable_function
233233
234234
\*******************************************************************/
235235

236-
static void json_output_unreachable_function(
236+
static void json_output_function(
237237
const irep_idt &function,
238238
const source_locationt &first_location,
239239
const source_locationt &last_location,
@@ -254,7 +254,7 @@ static void json_output_unreachable_function(
254254

255255
/*******************************************************************\
256256
257-
Function: unreachable_functions
257+
Function: list_functions
258258
259259
Inputs:
260260
@@ -264,10 +264,11 @@ Function: unreachable_functions
264264
265265
\*******************************************************************/
266266

267-
void unreachable_functions(
267+
static void list_functions(
268268
const goto_modelt &goto_model,
269269
const bool json,
270-
std::ostream &os)
270+
std::ostream &os,
271+
bool unreachable)
271272
{
272273
json_arrayt json_result;
273274

@@ -282,8 +283,9 @@ void unreachable_functions(
282283

283284
// f_it->first may be a link-time renamed version, use the
284285
// base_name instead; do not list inlined functions
285-
if(called.find(decl.base_name)!=called.end() ||
286-
f_it->second.is_inlined())
286+
if(unreachable ==
287+
(called.find(decl.base_name)!=called.end() ||
288+
f_it->second.is_inlined()))
287289
continue;
288290

289291
source_locationt first_location=decl.location;
@@ -315,7 +317,7 @@ void unreachable_functions(
315317
<< last_location.get_line() << "\n";
316318
}
317319
else
318-
json_output_unreachable_function(
320+
json_output_function(
319321
decl.base_name,
320322
first_location,
321323
last_location,
@@ -325,3 +327,43 @@ void unreachable_functions(
325327
if(json && !json_result.array.empty())
326328
os << json_result << std::endl;
327329
}
330+
331+
/*******************************************************************\
332+
333+
Function: unreachable_functions
334+
335+
Inputs:
336+
337+
Outputs:
338+
339+
Purpose:
340+
341+
\*******************************************************************/
342+
343+
void unreachable_functions(
344+
const goto_modelt &goto_model,
345+
const bool json,
346+
std::ostream &os)
347+
{
348+
list_functions(goto_model, json, os, true);
349+
}
350+
351+
/*******************************************************************\
352+
353+
Function: reachable_functions
354+
355+
Inputs:
356+
357+
Outputs:
358+
359+
Purpose:
360+
361+
\*******************************************************************/
362+
363+
void reachable_functions(
364+
const goto_modelt &goto_model,
365+
const bool json,
366+
std::ostream &os)
367+
{
368+
list_functions(goto_model, json, os, false);
369+
}

src/goto-analyzer/unreachable_instructions.h

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,4 +25,9 @@ void unreachable_functions(
2525
const bool json,
2626
std::ostream &os);
2727

28+
void reachable_functions(
29+
const goto_modelt &,
30+
const bool json,
31+
std::ostream &os);
32+
2833
#endif // CPROVER_GOTO_ANALYZER_UNREACHABLE_INSTRUCTIONS_H

0 commit comments

Comments
 (0)