Skip to content

Commit 0fbb98b

Browse files
committed
Cleanup options handling of count-eloc, list-eloc, print-path-lengths
1 parent 2ad157f commit 0fbb98b

File tree

4 files changed

+21
-9
lines changed

4 files changed

+21
-9
lines changed

src/goto-instrument/count_eloc.cpp

Lines changed: 1 addition & 0 deletions
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

Lines changed: 13 additions & 1 deletion
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

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,6 @@ Author: Daniel Kroening, kroening@kroening.com
8888
#include "wmm/weak_memory.h"
8989
#include "call_sequences.h"
9090
#include "accelerate/accelerate.h"
91-
#include "count_eloc.h"
9291
#include "horn_encoding.h"
9392
#include "thread_instrumentation.h"
9493
#include "skip_loops.h"
@@ -1480,15 +1479,14 @@ void goto_instrument_parse_optionst::help()
14801479
" --dump-cpp generate C++ source\n"
14811480
" --dot generate CFG graph in DOT format\n"
14821481
" --interpreter do concrete execution\n"
1483-
" --count-eloc count effective lines of code\n"
1484-
" --list-eloc list full path names of lines containing code\n" // NOLINT(*)
14851482
"\n"
14861483
"Diagnosis:\n"
14871484
" --show-loops show the loops in the program\n"
14881485
HELP_SHOW_PROPERTIES
14891486
" --show-symbol-table show loaded symbol table\n"
14901487
" --list-symbols list symbols with type information\n"
14911488
HELP_SHOW_GOTO_FUNCTIONS
1489+
HELP_GOTO_PROGRAM_STATS
14921490
" --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
14931491
" --print-internal-representation\n" // NOLINTNEXTLINE(*)
14941492
" show verbose internal representation of the program\n"
@@ -1497,8 +1495,6 @@ void goto_instrument_parse_optionst::help()
14971495
" --show-natural-loops show natural loop heads\n"
14981496
// NOLINTNEXTLINE(whitespace/line_length)
14991497
" --list-calls-args list all function calls with their arguments\n"
1500-
// NOLINTNEXTLINE(whitespace/line_length)
1501-
" --print-path-lengths print statistics about control-flow graph paths\n"
15021498
" --call-graph show graph of function calls\n"
15031499
// NOLINTNEXTLINE(whitespace/line_length)
15041500
" --reachable-call-graph show graph of function calls potentially reachable from main function\n"

src/goto-instrument/goto_instrument_parse_options.h

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,8 @@ Author: Daniel Kroening, kroening@kroening.com
2626

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

29+
#include "count_eloc.h"
30+
2931
// clang-format off
3032
#define GOTO_INSTRUMENT_OPTIONS \
3133
"(all)" \
@@ -80,17 +82,18 @@ Author: Daniel Kroening, kroening@kroening.com
8082
"(accelerate)(constant-propagator)" \
8183
"(k-induction):(step-case)(base-case)" \
8284
"(show-call-sequences)(check-call-sequence)" \
83-
"(interpreter)(show-reaching-definitions)(count-eloc)(list-eloc)" \
85+
"(interpreter)(show-reaching-definitions)" \
8486
"(list-symbols)(list-undefined-functions)" \
8587
"(z3)(add-library)(show-dependence-graph)" \
8688
"(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \
87-
"(show-threaded)(list-calls-args)(print-path-lengths)" \
89+
"(show-threaded)(list-calls-args)" \
8890
"(undefined-function-is-assume-false)" \
8991
"(remove-function-body):"\
9092
OPT_FLUSH \
9193
"(splice-call):" \
9294
OPT_REMOVE_CALLS_NO_BODY \
93-
OPT_REPLACE_FUNCTION_BODY
95+
OPT_REPLACE_FUNCTION_BODY \
96+
OPT_GOTO_PROGRAM_STATS
9497

9598
// clang-format on
9699

0 commit comments

Comments
 (0)