Skip to content

Commit 6aeac5e

Browse files
tautschnigtautschnig
authored
Merge pull request #6513 from tautschnig/jdiff-cleanup
jdiff: Remove processing of unsupported options
2 parents c05708c + 5019d02 commit 6aeac5e

File tree

4 files changed

+50
-136
lines changed

4 files changed

+50
-136
lines changed

‎jbmc/src/jdiff/jdiff_parse_options.cpp

Lines changed: 45 additions & 136 deletions
Original file line numberDiff line numberDiff line change
@@ -24,13 +24,10 @@ Author: Peter Schrammel
2424
#include <goto-programs/instrument_preconditions.h>
2525
#include <goto-programs/loop_ids.h>
2626
#include <goto-programs/mm_io.h>
27-
#include <goto-programs/remove_complex.h>
2827
#include <goto-programs/remove_function_pointers.h>
2928
#include <goto-programs/remove_returns.h>
3029
#include <goto-programs/remove_skip.h>
31-
#include <goto-programs/remove_vector.h>
3230
#include <goto-programs/remove_virtual_functions.h>
33-
#include <goto-programs/rewrite_union.h>
3431
#include <goto-programs/set_properties.h>
3532
#include <goto-programs/show_properties.h>
3633

@@ -71,88 +68,9 @@ void jdiff_parse_optionst::get_command_line_options(optionst &options)
7168
if(cmdline.isset("cover"))
7269
parse_cover_options(cmdline, options);
7370

74-
if(cmdline.isset("mm"))
75-
options.set_option("mm", cmdline.get_value("mm"));
76-
7771
// all checks supported by goto_check
7872
PARSE_OPTIONS_GOTO_CHECK_JAVA(cmdline, options);
7973

80-
if(cmdline.isset("debug-level"))
81-
options.set_option("debug-level", cmdline.get_value("debug-level"));
82-
83-
if(cmdline.isset("unwindset"))
84-
options.set_option("unwindset", cmdline.get_value("unwindset"));
85-
86-
// constant propagation
87-
if(cmdline.isset("no-propagation"))
88-
options.set_option("propagation", false);
89-
else
90-
options.set_option("propagation", true);
91-
92-
// check array bounds
93-
if(cmdline.isset("bounds-check"))
94-
options.set_option("bounds-check", true);
95-
else
96-
options.set_option("bounds-check", false);
97-
98-
// check division by zero
99-
if(cmdline.isset("div-by-zero-check"))
100-
options.set_option("div-by-zero-check", true);
101-
else
102-
options.set_option("div-by-zero-check", false);
103-
104-
// check overflow/underflow
105-
if(cmdline.isset("signed-overflow-check"))
106-
options.set_option("signed-overflow-check", true);
107-
else
108-
options.set_option("signed-overflow-check", false);
109-
110-
// check overflow/underflow
111-
if(cmdline.isset("unsigned-overflow-check"))
112-
options.set_option("unsigned-overflow-check", true);
113-
else
114-
options.set_option("unsigned-overflow-check", false);
115-
116-
// check overflow/underflow
117-
if(cmdline.isset("float-overflow-check"))
118-
options.set_option("float-overflow-check", true);
119-
else
120-
options.set_option("float-overflow-check", false);
121-
122-
// check for NaN (not a number)
123-
if(cmdline.isset("nan-check"))
124-
options.set_option("nan-check", true);
125-
else
126-
options.set_option("nan-check", false);
127-
128-
// check pointers
129-
if(cmdline.isset("pointer-check"))
130-
options.set_option("pointer-check", true);
131-
else
132-
options.set_option("pointer-check", false);
133-
134-
// check for memory leaks
135-
if(cmdline.isset("memory-leak-check"))
136-
options.set_option("memory-leak-check", true);
137-
else
138-
options.set_option("memory-leak-check", false);
139-
140-
// check assertions
141-
if(cmdline.isset("no-assertions"))
142-
options.set_option("assertions", false);
143-
else
144-
options.set_option("assertions", true);
145-
146-
// use assumptions
147-
if(cmdline.isset("no-assumptions"))
148-
options.set_option("assumptions", false);
149-
else
150-
options.set_option("assumptions", true);
151-
152-
// magic error label
153-
if(cmdline.isset("error-label"))
154-
options.set_option("error-label", cmdline.get_values("error-label"));
155-
15674
options.set_option("show-properties", cmdline.isset("show-properties"));
15775
}
15876

@@ -247,73 +165,64 @@ bool jdiff_parse_optionst::process_goto_program(
247165
const optionst &options,
248166
goto_modelt &goto_model)
249167
{
250-
{
251-
// remove function pointers
252-
log.status() << "Removing function pointers and virtual functions"
253-
<< messaget::eom;
254-
remove_function_pointers(
255-
ui_message_handler, goto_model, cmdline.isset("pointer-check"));
168+
// remove function pointers
169+
log.status() << "Removing function pointers and virtual functions"
170+
<< messaget::eom;
171+
remove_function_pointers(
172+
ui_message_handler, goto_model, cmdline.isset("pointer-check"));
256173

257-
// Java virtual functions -> explicit dispatch tables:
258-
remove_virtual_functions(goto_model);
174+
// Java virtual functions -> explicit dispatch tables:
175+
remove_virtual_functions(goto_model);
259176

260-
// remove Java throw and catch
261-
// This introduces instanceof, so order is important:
262-
remove_exceptions_using_instanceof(goto_model, ui_message_handler);
177+
// remove Java throw and catch
178+
// This introduces instanceof, so order is important:
179+
remove_exceptions_using_instanceof(goto_model, ui_message_handler);
263180

264-
// Java instanceof -> clsid comparison:
265-
class_hierarchyt class_hierarchy(goto_model.symbol_table);
266-
remove_instanceof(goto_model, class_hierarchy, ui_message_handler);
181+
// Java instanceof -> clsid comparison:
182+
class_hierarchyt class_hierarchy(goto_model.symbol_table);
183+
remove_instanceof(goto_model, class_hierarchy, ui_message_handler);
267184

268-
mm_io(goto_model);
185+
mm_io(goto_model);
269186

270-
// instrument library preconditions
271-
instrument_preconditions(goto_model);
187+
// instrument library preconditions
188+
instrument_preconditions(goto_model);
272189

273-
// remove returns, gcc vectors, complex
274-
remove_returns(goto_model);
275-
remove_vector(goto_model);
276-
remove_complex(goto_model);
277-
rewrite_union(goto_model);
190+
// remove returns
191+
remove_returns(goto_model);
278192

279-
// add generic checks
280-
log.status() << "Generic Property Instrumentation" << messaget::eom;
281-
goto_check_java(options, goto_model, ui_message_handler);
193+
// add generic checks
194+
log.status() << "Generic Property Instrumentation" << messaget::eom;
195+
goto_check_java(options, goto_model, ui_message_handler);
282196

283-
// checks don't know about adjusted float expressions
284-
adjust_float_expressions(goto_model);
197+
// checks don't know about adjusted float expressions
198+
adjust_float_expressions(goto_model);
285199

286-
// recalculate numbers, etc.
287-
goto_model.goto_functions.update();
200+
// recalculate numbers, etc.
201+
goto_model.goto_functions.update();
288202

289-
// add loop ids
290-
goto_model.goto_functions.compute_loop_numbers();
291-
292-
// remove skips such that trivial GOTOs are deleted and not considered
293-
// for coverage annotation:
203+
// instrument cover goals
204+
if(cmdline.isset("cover"))
205+
{
206+
// remove skips such that trivial GOTOs are deleted and not considered for
207+
// coverage annotation:
294208
remove_skip(goto_model);
295209

296-
// instrument cover goals
297-
if(cmdline.isset("cover"))
298-
{
299-
const auto cover_config =
300-
get_cover_config(options, goto_model.symbol_table, ui_message_handler);
301-
if(instrument_cover_goals(cover_config, goto_model, ui_message_handler))
302-
return true;
303-
}
304-
305-
// label the assertions
306-
// This must be done after adding assertions and
307-
// before using the argument of the "property" option.
308-
// Do not re-label after using the property slicer because
309-
// this would cause the property identifiers to change.
310-
label_properties(goto_model);
311-
312-
// remove any skips introduced since coverage instrumentation
313-
remove_skip(goto_model);
314-
goto_model.goto_functions.update();
210+
const auto cover_config =
211+
get_cover_config(options, goto_model.symbol_table, ui_message_handler);
212+
if(instrument_cover_goals(cover_config, goto_model, ui_message_handler))
213+
return true;
315214
}
316215

216+
// label the assertions
217+
// This must be done after adding assertions and
218+
// before using the argument of the "property" option.
219+
// Do not re-label after using the property slicer because
220+
// this would cause the property identifiers to change.
221+
label_properties(goto_model);
222+
223+
// remove any skips introduced since coverage instrumentation
224+
remove_skip(goto_model);
225+
317226
return false;
318227
}
319228

@@ -335,7 +244,7 @@ void jdiff_parse_optionst::help()
335244
"Diff options:\n"
336245
HELP_SHOW_GOTO_FUNCTIONS
337246
HELP_SHOW_PROPERTIES
338-
" --syntactic do syntactic diff (default)\n"
247+
" --show-loops show the loops in the programs\n"
339248
" -u | --unified output unified diff\n"
340249
" --change-impact | \n"
341250
" --forward-impact |\n"

‎jbmc/src/jdiff/jdiff_parse_options.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@ class goto_modelt;
2929
"(json-ui)" \
3030
OPT_SHOW_GOTO_FUNCTIONS \
3131
OPT_SHOW_PROPERTIES \
32+
"(show-loops)" \
3233
OPT_GOTO_CHECK_JAVA \
3334
OPT_COVER \
3435
"(verbosity):(version)" \

‎src/goto-diff/goto_diff_parse_options.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -64,6 +64,8 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options)
6464
// all checks supported by goto_check
6565
PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
6666

67+
options.set_option("show-properties", cmdline.isset("show-properties"));
68+
6769
// Options for process_goto_program
6870
options.set_option("rewrite-union", true);
6971
}
@@ -224,6 +226,7 @@ void goto_diff_parse_optionst::help()
224226
"\n"
225227
"Diff options:\n"
226228
HELP_SHOW_GOTO_FUNCTIONS
229+
HELP_SHOW_PROPERTIES
227230
" --show-loops show the loops in the programs\n"
228231
" -u | --unified output unified diff\n"
229232
" --change-impact | \n"

‎src/goto-diff/goto_diff_parse_options.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,7 @@ class optionst;
3030
#define GOTO_DIFF_OPTIONS \
3131
"(json-ui)" \
3232
OPT_SHOW_GOTO_FUNCTIONS \
33+
OPT_SHOW_PROPERTIES \
3334
"(show-loops)" \
3435
OPT_GOTO_CHECK \
3536
OPT_COVER \

0 commit comments

Comments
 (0)