Skip to content

Commit d8c5a98

Browse files
committed
Cleanup options handling of count-eloc, list-eloc, print-path-lengths
1 parent 6882da6 commit d8c5a98

File tree

4 files changed

+21
-9
lines changed

4 files changed

+21
-9
lines changed

src/goto-instrument/count_eloc.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ Date: December 2012
2020
#include <util/file_util.h>
2121

2222
#include <goto-programs/cfg.h>
23+
#include <goto-programs/goto_model.h>
2324

2425
typedef std::unordered_set<irep_idt> linest;
2526
typedef std::unordered_map<irep_idt, linest> filest;

src/goto-instrument/count_eloc.h

+13-1
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,22 @@ Date: December 2012
1414
#ifndef CPROVER_GOTO_INSTRUMENT_COUNT_ELOC_H
1515
#define CPROVER_GOTO_INSTRUMENT_COUNT_ELOC_H
1616

17-
#include <goto-programs/goto_model.h>
17+
class goto_modelt;
1818

1919
void count_eloc(const goto_modelt &);
2020
void list_eloc(const goto_modelt &);
2121
void print_path_lengths(const goto_modelt &);
2222

23+
#define OPT_GOTO_PROGRAM_STATS \
24+
"(count-eloc)" \
25+
"(list-eloc)" \
26+
"(print-path-lengths)"
27+
28+
#define HELP_GOTO_PROGRAM_STATS \
29+
" --count-eloc count effective lines of code\n" \
30+
" --list-eloc list full path names of lines " \
31+
"containing code\n" \
32+
" --print-path-lengths print statistics about control-flow graph " \
33+
"paths\n"
34+
2335
#endif // CPROVER_GOTO_INSTRUMENT_COUNT_ELOC_H

src/goto-instrument/goto_instrument_parse_options.cpp

+1-5
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,6 @@ Author: Daniel Kroening, [email protected]
9191
#include "wmm/weak_memory.h"
9292
#include "call_sequences.h"
9393
#include "accelerate/accelerate.h"
94-
#include "count_eloc.h"
9594
#include "horn_encoding.h"
9695
#include "thread_instrumentation.h"
9796
#include "skip_loops.h"
@@ -1454,15 +1453,14 @@ void goto_instrument_parse_optionst::help()
14541453
" --dump-cpp generate C++ source\n"
14551454
" --dot generate CFG graph in DOT format\n"
14561455
" --interpreter do concrete execution\n"
1457-
" --count-eloc count effective lines of code\n"
1458-
" --list-eloc list full path names of lines containing code\n" // NOLINT(*)
14591456
"\n"
14601457
"Diagnosis:\n"
14611458
" --show-loops show the loops in the program\n"
14621459
HELP_SHOW_PROPERTIES
14631460
" --show-symbol-table show loaded symbol table\n"
14641461
" --list-symbols list symbols with type information\n"
14651462
HELP_SHOW_GOTO_FUNCTIONS
1463+
HELP_GOTO_PROGRAM_STATS
14661464
" --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
14671465
" --print-internal-representation\n" // NOLINTNEXTLINE(*)
14681466
" show verbose internal representation of the program\n"
@@ -1471,8 +1469,6 @@ void goto_instrument_parse_optionst::help()
14711469
" --show-natural-loops show natural loop heads\n"
14721470
// NOLINTNEXTLINE(whitespace/line_length)
14731471
" --list-calls-args list all function calls with their arguments\n"
1474-
// NOLINTNEXTLINE(whitespace/line_length)
1475-
" --print-path-lengths print statistics about control-flow graph paths\n"
14761472
" --call-graph show graph of function calls\n"
14771473
// NOLINTNEXTLINE(whitespace/line_length)
14781474
" --reachable-call-graph show graph of function calls potentially reachable from main function\n"

src/goto-instrument/goto_instrument_parse_options.h

+6-3
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,8 @@ Author: Daniel Kroening, [email protected]
2727

2828
#include <goto-programs/generate_function_bodies.h>
2929

30+
#include "count_eloc.h"
31+
3032
// clang-format off
3133
#define GOTO_INSTRUMENT_OPTIONS \
3234
"(all)" \
@@ -81,17 +83,18 @@ Author: Daniel Kroening, [email protected]
8183
"(accelerate)(constant-propagator)" \
8284
"(k-induction):(step-case)(base-case)" \
8385
"(show-call-sequences)(check-call-sequence)" \
84-
"(interpreter)(show-reaching-definitions)(count-eloc)(list-eloc)" \
86+
"(interpreter)(show-reaching-definitions)" \
8587
"(list-symbols)(list-undefined-functions)" \
8688
"(z3)(add-library)(show-dependence-graph)" \
8789
"(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \
88-
"(show-threaded)(list-calls-args)(print-path-lengths)" \
90+
"(show-threaded)(list-calls-args)" \
8991
"(undefined-function-is-assume-false)" \
9092
"(remove-function-body):"\
9193
OPT_FLUSH \
9294
"(splice-call):" \
9395
OPT_REMOVE_CALLS_NO_BODY \
94-
OPT_REPLACE_FUNCTION_BODY
96+
OPT_REPLACE_FUNCTION_BODY \
97+
OPT_GOTO_PROGRAM_STATS
9598

9699
// clang-format on
97100

0 commit comments

Comments
 (0)