cprover
Loading...
Searching...
No Matches
jdiff_parse_options.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: JDIFF Command Line Option Processing
4
5Author: Peter Schrammel
6
7\*******************************************************************/
8
11
12#include "jdiff_parse_options.h"
13
14#include <util/config.h>
15#include <util/exit_codes.h>
16#include <util/help_formatter.h>
17#include <util/options.h>
18#include <util/version.h>
19
25#include <goto-programs/mm_io.h>
32
39
40#include "java_syntactic_diff.h"
41
42#include <cstdlib> // exit()
43#include <iostream>
44
48 argc,
49 argv,
50 std::string("JDIFF ") + CBMC_VERSION)
51{
52}
53
55{
56 if(config.set(cmdline))
57 {
59 exit(1);
60 }
61
63
64 // check assertions
65 if(cmdline.isset("no-assertions"))
66 options.set_option("assertions", false);
67 else
68 options.set_option("assertions", true);
69
70 // use assumptions
71 if(cmdline.isset("no-assumptions"))
72 options.set_option("assumptions", false);
73 else
74 options.set_option("assumptions", true);
75
76 if(cmdline.isset("cover"))
78
79 options.set_option("show-properties", cmdline.isset("show-properties"));
80}
81
84{
85 if(cmdline.isset("version"))
86 {
87 std::cout << CBMC_VERSION << '\n';
89 }
90
91 //
92 // command line options
93 //
94
95 optionst options;
99
101
102 if(cmdline.args.size() != 2)
103 {
104 log.error() << "Please provide two programs to compare" << messaget::eom;
106 }
107
109
110 goto_modelt goto_model1 =
112 if(process_goto_program(options, goto_model1))
114 goto_modelt goto_model2 =
116 if(process_goto_program(options, goto_model2))
118
119 if(cmdline.isset("show-loops"))
120 {
124 }
125
126 if(
127 cmdline.isset("show-goto-functions") ||
128 cmdline.isset("list-goto-functions"))
129 {
131 goto_model1, ui_message_handler, cmdline.isset("list-goto-functions"));
133 goto_model2, ui_message_handler, cmdline.isset("list-goto-functions"));
135 }
136
137 if(
138 cmdline.isset("change-impact") || cmdline.isset("forward-impact") ||
139 cmdline.isset("backward-impact"))
140 {
141 impact_modet impact_mode =
142 cmdline.isset("forward-impact")
144 : (cmdline.isset("backward-impact") ? impact_modet::BACKWARD
147 goto_model1, goto_model2, impact_mode, cmdline.isset("compact-output"));
148
150 }
151
152 if(cmdline.isset("unified") || cmdline.isset('u'))
153 {
154 unified_difft u(goto_model1, goto_model2);
155 u();
156 u.output(std::cout);
157
159 }
160
162 goto_model1, goto_model2, options, ui_message_handler);
163 sd();
164 sd.output_functions();
165
167}
168
170 const optionst &options,
171 goto_modelt &goto_model)
172{
173 // remove function pointers
174 log.status() << "Removing function pointers and virtual functions"
175 << messaget::eom;
177
178 // Java virtual functions -> explicit dispatch tables:
179 remove_virtual_functions(goto_model);
180
181 // remove Java throw and catch
182 // This introduces instanceof, so order is important:
184
185 // Java instanceof -> clsid comparison:
186 class_hierarchyt class_hierarchy(goto_model.symbol_table);
187 remove_instanceof(goto_model, class_hierarchy, ui_message_handler);
188
189 mm_io(goto_model);
190
191 // instrument library preconditions
192 instrument_preconditions(goto_model);
193
194 // remove returns
195 remove_returns(goto_model);
196
197 transform_assertions_assumptions(options, goto_model);
198
199 // checks don't know about adjusted float expressions
200 adjust_float_expressions(goto_model);
201
202 // recalculate numbers, etc.
203 goto_model.goto_functions.update();
204
205 // instrument cover goals
206 if(cmdline.isset("cover"))
207 {
208 // remove skips such that trivial GOTOs are deleted and not considered for
209 // coverage annotation:
210 remove_skip(goto_model);
211
212 const auto cover_config =
214 if(instrument_cover_goals(cover_config, goto_model, ui_message_handler))
215 return true;
216 }
217
218 // label the assertions
219 // This must be done after adding assertions and
220 // before using the argument of the "property" option.
221 // Do not re-label after using the property slicer because
222 // this would cause the property identifiers to change.
223 label_properties(goto_model);
224
225 // remove any skips introduced since coverage instrumentation
226 remove_skip(goto_model);
227
228 return false;
229}
230
233{
234 // clang-format off
235 std::cout << '\n' << banner_string("JDIFF", CBMC_VERSION) << '\n'
236 << align_center_with_border("Copyright (C) 2016-2018") << '\n'
237 << align_center_with_border("Daniel Kroening, Peter Schrammel") << '\n' // NOLINT(*)
238 << align_center_with_border("kroening@kroening.com") << '\n';
239
240 std::cout << help_formatter(
241 "\n"
242 "Usage: \tPurpose:\n"
243 "\n"
244 " {bjdiff} [{y-?}] [{y-h}] [{y--help}] \t show this help\n"
245 " {bjdiff} {uold} {unew} \t jars to be compared\n"
246 "\n"
247 "Diff options:\n"
250 " {y--show-loops} \t show the loops in the programs\n"
251 " {y-u}, {y--unified} \t output unified diff\n"
252 " {y--change-impact}, {y--forward-impact}, {y--backward-impact} \t output"
253 " unified diff with forward&backward/forward/backward dependencies\n"
254 " {y--compact-output} \t output dependencies in compact mode\n"
255 "\n"
256 "Program instrumentation options:\n"
257 " {y--no-assertions} \t ignore user assertions\n"
258 " {y--no-assumptions} \t ignore user assumptions\n"
260 "\n"
261 "Other options:\n"
262 " {y--version} \t show version and exit\n"
263 " {y--json-ui} \t use JSON-formatted output\n"
264 " {y--verbosity} {u#} \t verbosity level\n"
266 "\n");
267 // clang-format on
268}
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Symbolic Execution.
configt config
Definition config.cpp:25
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
Non-graph-based representation of the class hierarchy.
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
virtual void output_functions() const
Output diff result.
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
jdiff_parse_optionst(int argc, const char **argv)
void register_languages() override
void help() override
display command line help
bool process_goto_program(const optionst &options, goto_modelt &goto_model)
void get_command_line_options(optionst &options)
int doit() override
invoke main modules
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
virtual uit get_ui() const
Definition ui_message.h:33
void output(std::ostream &os) const
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:33
static void show_goto_functions(const goto_modelt &goto_model)
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
static void transform_assertions_assumptions(goto_programt &goto_program, bool enable_assertions, bool enable_built_in_assertions, bool enable_assumptions)
Checks for Errors in C and Java Programs.
Help Formatter.
static help_formattert help_formatter(const std::string &s)
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Initialize a Goto Program.
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
void parse_java_language_options(const cmdlinet &cmd, optionst &options)
Parse options that are java bytecode specific.
Syntactic GOTO-DIFF for Java.
JDIFF Command Line Option Processing.
#define JDIFF_OPTIONS
void show_loop_ids(ui_message_handlert::uit ui, const goto_modelt &goto_model)
Definition loop_ids.cpp:21
Loop IDs.
void mm_io(const exprt &mm_io_r, const exprt &mm_io_r_value, const exprt &mm_io_w, goto_functionst::goto_functiont &goto_function, const namespacet &ns)
Definition mm_io.cpp:36
Perform Memory-mapped I/O instrumentation.
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_exceptions_using_instanceof(symbol_table_baset &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler)
removes throws/CATCH-POP/CATCH-PUSH
Remove function exceptional returns.
void remove_function_pointers(message_handlert &_message_handler, goto_modelt &goto_model, bool only_remove_const_fps)
Remove Indirect Function Calls.
void remove_instanceof(const irep_idt &function_identifier, goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, message_handlert &message_handler)
Replace an instanceof in the expression or guard of the passed instruction of the given function body...
Remove Instance-of Operators.
void remove_returns(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
removes returns
Replace function returns by assignments to global variables.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
void remove_virtual_functions(symbol_table_baset &symbol_table, goto_functionst &goto_functions)
Remove virtual function calls from all functions in the specified list and replace them with their mo...
Functions for replacing virtual function call with a static function calls in functions,...
void label_properties(goto_modelt &goto_model)
Set the properties to check.
#define HELP_SHOW_GOTO_FUNCTIONS
Show the properties.
#define HELP_SHOW_PROPERTIES
#define HELP_TIMESTAMP
Definition timestamper.h:14
Unified diff (using LCSS) of goto functions.
const char * CBMC_VERSION