cprover
goto_diff_parse_options.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: GOTO-DIFF Command Line Option Processing
4
5Author: Peter Schrammel
6
7\*******************************************************************/
8
11
13
14#include <cstdlib> // exit()
15#include <fstream>
16#include <iostream>
17
18#include <util/config.h>
19#include <util/exit_codes.h>
20#include <util/options.h>
21#include <util/version.h>
22
30
32
34
36
37#include <cpp/cprover_library.h>
38
39#include "syntactic_diff.h"
40#include "unified_diff.h"
41#include "change_impact.h"
42
46 argc,
47 argv,
48 std::string("GOTO-DIFF ") + CBMC_VERSION)
49{
50}
51
53{
54 if(config.set(cmdline))
55 {
57 exit(1);
58 }
59
60 if(cmdline.isset("cover"))
62
63 // all checks supported by goto_check
65
66 options.set_option("show-properties", cmdline.isset("show-properties"));
67
68 // Options for process_goto_program
69 options.set_option("rewrite-union", true);
70}
71
74{
75 if(cmdline.isset("version"))
76 {
77 std::cout << CBMC_VERSION << '\n';
79 }
80
81 //
82 // command line options
83 //
84
85 optionst options;
89
91
92 if(cmdline.args.size()!=2)
93 {
94 log.error() << "Please provide two programs to compare" << messaget::eom;
96 }
97
99
100 goto_modelt goto_model1 =
102 if(process_goto_program(options, goto_model1))
104 goto_modelt goto_model2 =
106 if(process_goto_program(options, goto_model2))
108
109 if(cmdline.isset("show-loops"))
110 {
114 }
115
116 if(
117 cmdline.isset("show-goto-functions") ||
118 cmdline.isset("list-goto-functions"))
119 {
121 goto_model1, ui_message_handler, cmdline.isset("list-goto-functions"));
123 goto_model2, ui_message_handler, cmdline.isset("list-goto-functions"));
125 }
126
127 if(cmdline.isset("change-impact") ||
128 cmdline.isset("forward-impact") ||
129 cmdline.isset("backward-impact"))
130 {
131 impact_modet impact_mode=
132 cmdline.isset("forward-impact") ?
134 (cmdline.isset("backward-impact") ?
138 goto_model1,
139 goto_model2,
140 impact_mode,
141 cmdline.isset("compact-output"));
142
144 }
145
146 if(cmdline.isset("unified") ||
147 cmdline.isset('u'))
148 {
149 unified_difft u(goto_model1, goto_model2);
150 u();
151 u.output(std::cout);
152
154 }
155
156 syntactic_difft sd(goto_model1, goto_model2, options, ui_message_handler);
157 sd();
158 sd.output_functions();
159
161}
162
164 const optionst &options,
165 goto_modelt &goto_model)
166{
167 // Remove inline assembler; this needs to happen before
168 // adding the library.
169 remove_asm(goto_model);
170
171 // add the library
172 log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
173 << messaget::eom;
176
177 // Common removal of types and complex constructs
178 if(::process_goto_program(goto_model, options, log))
179 return true;
180
181 // instrument cover goals
182 if(cmdline.isset("cover"))
183 {
184 // remove skips such that trivial GOTOs are deleted and not considered
185 // for coverage annotation:
186 remove_skip(goto_model);
187
188 const auto cover_config =
190 if(instrument_cover_goals(cover_config, goto_model, ui_message_handler))
191 return true;
192
193 goto_model.goto_functions.update();
194 }
195
196 // label the assertions
197 // This must be done after adding assertions and
198 // before using the argument of the "property" option.
199 // Do not re-label after using the property slicer because
200 // this would cause the property identifiers to change.
201 label_properties(goto_model);
202
203 // remove any skips introduced since coverage instrumentation
204 remove_skip(goto_model);
205
206 return false;
207}
208
211{
212 // clang-format off
213 std::cout << '\n' << banner_string("GOTO_DIFF", CBMC_VERSION) << '\n'
214 << align_center_with_border("Copyright (C) 2016") << '\n'
215 << align_center_with_border("Daniel Kroening, Peter Schrammel") << '\n' // NOLINT (*)
216 << align_center_with_border("kroening@kroening.com") << '\n'
217 <<
218 "\n"
219 "Usage: Purpose:\n"
220 "\n"
221 " goto_diff [-?] [-h] [--help] show help\n"
222 " goto_diff old new goto binaries to be compared\n"
223 "\n"
224 "Diff options:\n"
227 " --show-loops show the loops in the programs\n"
228 " -u | --unified output unified diff\n"
229 " --change-impact | \n"
230 " --forward-impact |\n"
231 // NOLINTNEXTLINE(whitespace/line_length)
232 " --backward-impact output unified diff with forward&backward/forward/backward dependencies\n"
233 " --compact-output output dependencies in compact mode\n"
234 "\n"
235 "Program instrumentation options:\n"
238 "\n"
239 "Other options:\n"
240 " --version show version and exit\n"
241 " --json-ui use JSON-formatted output\n"
244 "\n";
245 // clang-format on
246}
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
void change_impact(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output)
Data and control-dependencies of syntactic diff.
impact_modet
Definition: change_impact.h:18
std::string get_value(char option) const
Definition: cmdline.cpp:48
virtual bool isset(char option) const
Definition: cmdline.cpp:30
argst args
Definition: cmdline.h:145
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
struct configt::ansi_ct ansi_c
int doit() override
invoke main modules
bool process_goto_program(const optionst &options, goto_modelt &goto_model)
void help() override
display command line help
goto_diff_parse_optionst(int argc, const char **argv)
void get_command_line_options(optionst &options)
virtual void output_functions() const
Output diff result.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
static unsigned eval_verbosity(const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.
Definition: message.cpp:105
mstreamt & error() const
Definition: message.h:399
@ M_STATISTICS
Definition: message.h:171
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
virtual void usage_error()
void log_version_and_architecture(const std::string &front_end)
Write version and system architecture to log.status().
ui_message_handlert ui_message_handler
Definition: parse_options.h:45
virtual uit get_ui() const
Definition: ui_message.h:33
void output(std::ostream &os) const
configt config
Definition: config.cpp:25
static void instrument_cover_goals(const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenterst &instrumenters, const irep_idt &mode, message_handlert &message_handler, const cover_instrumenter_baset::assertion_factoryt &make_assertion)
Applies instrumenters to given goto program.
Definition: cover.cpp:37
cover_configt get_cover_config(const optionst &options, const symbol_tablet &symbol_table, message_handlert &message_handler)
Build data structures controlling coverage from command-line options.
Definition: cover.cpp:186
void parse_cover_options(const cmdlinet &cmdline, optionst &options)
Parses coverage-related command line options.
Definition: cover.cpp:148
Coverage Instrumentation.
#define HELP_COVER
Definition: cover.h:32
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_INTERNAL_ERROR
An error has been encountered during processing the requested analysis.
Definition: exit_codes.h:45
#define CPROVER_EXIT_INCORRECT_TASK
The command line is correctly structured but cannot be carried out due to missing files,...
Definition: exit_codes.h:49
#define CPROVER_EXIT_SUCCESS
Success indicates the required analysis has been performed without error.
Definition: exit_codes.h:16
#define PARSE_OPTIONS_GOTO_CHECK(cmdline, options)
Definition: goto_check_c.h:74
#define HELP_GOTO_CHECK
Definition: goto_check_c.h:53
GOTO-DIFF Command Line Option Processing.
#define GOTO_DIFF_OPTIONS
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Initialize a Goto Program.
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition: loop_ids.cpp:21
Loop IDs.
STL namespace.
Options.
std::string align_center_with_border(const std::string &text)
Utility for displaying help centered messages borderered by "* *".
std::string banner_string(const std::string &front_end, const std::string &version)
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
Definition: remove_asm.cpp:512
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:88
Program Transformation.
void label_properties(goto_modelt &goto_model)
Set the properties to check.
void show_goto_functions(const namespacet &ns, ui_message_handlert &ui_message_handler, const goto_functionst &goto_functions, bool list_only)
#define HELP_SHOW_GOTO_FUNCTIONS
Show the properties.
#define HELP_SHOW_PROPERTIES
irep_idt arch
Definition: config.h:191
Syntactic GOTO-DIFF.
#define HELP_TIMESTAMP
Definition: timestamper.h:14
#define HELP_FLUSH
Definition: ui_message.h:108
Unified diff (using LCSS) of goto functions.
const char * CBMC_VERSION