Skip to content

Commit 556352d

Browse files
author
Daniel Kroening
authored
Merge pull request #724 from tautschnig/release-cleanup
Near-release cleanup
2 parents 7e24dca + 80ba3cf commit 556352d

File tree

12 files changed

+40
-19
lines changed

12 files changed

+40
-19
lines changed

‎CHANGELOG

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,9 @@
2020
* GOTO-CC: GCC-style error/warning messages
2121
* GOTO-CC: New options --native-compiler and --native-linker to select the
2222
compiler/linker to be used when building combined native/goto object files.
23+
* CBMC, SYMEX, GOTO-INSTRUMENT: New option --drop-unused-functions. Removed
24+
ambiguous --show-reachable-properties.
25+
* CBMC: New option --no-built-in-assertions
2326

2427

2528
5.6

‎regression/cbmc/Pointer_byte_extract9/main.c

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
#include <assert.h>
2+
13
int main()
24
{
35
int N;

‎regression/cbmc/graphml_witness1/test.desc

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -46,29 +46,29 @@ main.c
4646
<graph edgedefault="directed">
4747
<data key="sourcecodelang">C</data>
4848
<node id="sink"/>
49-
<node id="33.22">
49+
<node id="[0-9\.]*">
5050
<data key="entry">true</data>
5151
</node>
5252
<edge source="33.22" target="4.29">
5353
<data key="originfile">main.c</data>
5454
<data key="startline">21</data>
5555
</edge>
56-
<node id="4.29"/>
57-
<edge source="4.29" target="29.31">
56+
<node id="[0-9\.]*"/>
57+
<edge source="[0-9\.]*" target="[0-9\.]*">
5858
<data key="originfile">main.c</data>
5959
<data key="startline">29</data>
6060
<data key="assumption.scope">main</data>
6161
</edge>
62-
<node id="29.31"/>
63-
<edge source="29.31" target="5.33">
62+
<node id="[0-9\.]*"/>
63+
<edge source="[0-9\.]*" target="[0-9\.]*">
6464
<data key="originfile">main.c</data>
6565
<data key="startline">15</data>
6666
<data key="assumption.scope">remove_one</data>
6767
</edge>
68-
<node id="5.33">
68+
<node id="[0-9\.]*">
6969
<data key="violation">true</data>
7070
</node>
71-
<edge source="5.33" target="sink">
71+
<edge source="[0-9\.]*" target="sink">
7272
<data key="originfile">main.c</data>
7373
<data key="startline">31</data>
7474
</edge>

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -946,7 +946,7 @@ bool cbmc_parse_optionst::process_goto_program(
946946
if(cmdline.isset("drop-unused-functions"))
947947
{
948948
// Entry point will have been set before and function pointers removed
949-
status() << "Removing Unused Functions" << eom;
949+
status() << "Removing unused functions" << eom;
950950
remove_unused_functions(goto_functions, ui_message_handler);
951951
}
952952

@@ -1096,7 +1096,6 @@ void cbmc_parse_optionst::help()
10961096
" --property id only check one specific property\n"
10971097
" --stop-on-fail stop analysis once a failed property is detected\n" // NOLINT(*)
10981098
" --trace give a counterexample trace for failed properties\n" //NOLINT(*)
1099-
" --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
11001099
"\n"
11011100
"C/C++ frontend options:\n"
11021101
" -I path set include path (C/C++)\n"
@@ -1142,6 +1141,7 @@ void cbmc_parse_optionst::help()
11421141
" --show-parse-tree show parse tree\n"
11431142
" --show-symbol-table show symbol table\n"
11441143
HELP_SHOW_GOTO_FUNCTIONS
1144+
" --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
11451145
"\n"
11461146
"Program instrumentation options:\n"
11471147
HELP_GOTO_CHECK
@@ -1199,5 +1199,6 @@ void cbmc_parse_optionst::help()
11991199
" --xml-ui use XML-formatted output\n"
12001200
" --xml-interface bi-directional XML interface\n"
12011201
" --json-ui use JSON-formatted output\n"
1202+
" --verbosity # verbosity level\n"
12021203
"\n";
12031204
}

‎src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -744,6 +744,14 @@ int goto_instrument_parse_optionst::doit()
744744
return 0;
745745
}
746746

747+
if(cmdline.isset("drop-unused-functions"))
748+
{
749+
do_indirect_call_and_rtti_removal();
750+
751+
status() << "Removing unused functions" << eom;
752+
remove_unused_functions(goto_functions, get_message_handler());
753+
}
754+
747755
// write new binary?
748756
if(cmdline.args.size()==2)
749757
{
@@ -1182,6 +1190,9 @@ void goto_instrument_parse_optionst::instrument_goto_program()
11821190

11831191
if(cmdline.isset("string-abstraction"))
11841192
{
1193+
do_indirect_call_and_rtti_removal();
1194+
do_remove_returns();
1195+
11851196
status() << "String Abstraction" << eom;
11861197
string_abstraction(
11871198
symbol_table,

‎src/goto-instrument/goto_instrument_parse_options.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,7 @@ Author: Daniel Kroening, [email protected]
4545
"(stack-depth):(nondet-static)" \
4646
"(function-enter):(function-exit):(branch):" \
4747
OPT_SHOW_GOTO_FUNCTIONS \
48+
"(drop-unused-functions)" \
4849
"(show-value-sets)" \
4950
"(show-global-may-alias)" \
5051
"(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \

‎src/solvers/flattening/boolbv_floatbv_op.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -138,7 +138,7 @@ bvt boolbvt::convert_floatbv_op(const exprt &expr)
138138
else if(expr.id()==ID_floatbv_rem)
139139
return float_utils.rem(bv0, bv1);
140140
else
141-
assert(false);
141+
throw "unexpected operator "+expr.id_string();
142142
}
143143
else if(type.id()==ID_vector || type.id()==ID_complex)
144144
{

‎src/solvers/floatbv/float_utils.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -206,7 +206,7 @@ bvt float_utilst::to_integer(
206206
return result;
207207
}
208208
else
209-
assert(0);
209+
throw "unsupported rounding mode";
210210
}
211211

212212
/*******************************************************************\

‎src/symex/symex_parse_options.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -386,7 +386,7 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
386386
if(cmdline.isset("drop-unused-functions"))
387387
{
388388
// Entry point will have been set before and function pointers removed
389-
status() << "Removing Unused Functions" << eom;
389+
status() << "Removing unused functions" << eom;
390390
remove_unused_functions(goto_model.goto_functions, ui_message_handler);
391391
}
392392

@@ -690,7 +690,6 @@ void symex_parse_optionst::help()
690690
" --stop-on-fail stop analysis once a failed property is detected\n"
691691
// NOLINTNEXTLINE(whitespace/line_length)
692692
" --trace give a counterexample trace for failed properties\n"
693-
" --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
694693
"\n"
695694
"Frontend options:\n"
696695
" -I path set include path (C/C++)\n"
@@ -705,6 +704,7 @@ void symex_parse_optionst::help()
705704
" --show-parse-tree show parse tree\n"
706705
" --show-symbol-table show symbol table\n"
707706
HELP_SHOW_GOTO_FUNCTIONS
707+
" --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*)
708708
" --ppc-macos set MACOS/PPC architecture\n"
709709
" --mm model set memory model (default: sc)\n"
710710
" --arch set architecture (default: "
@@ -738,5 +738,6 @@ void symex_parse_optionst::help()
738738
"Other options:\n"
739739
" --version show version and exit\n"
740740
" --xml-ui use XML-formatted output\n"
741+
" --verbosity # verbosity level\n"
741742
"\n";
742743
}

‎src/util/irep.h

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -283,11 +283,7 @@ class irept
283283

284284
void clear()
285285
{
286-
#ifdef USE_DSTRING
287286
data.clear();
288-
#else
289-
data="";
290-
#endif
291287
sub.clear();
292288
named_sub.clear();
293289
comments.clear();

‎src/util/json_irep.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -164,8 +164,8 @@ void json_irept::convert_from_json(const jsont &in, irept &out) const
164164
}
165165

166166
for(const auto &named_sub : in["namedSub"].object)
167-
convert_from_json(named_sub.second, out.get_named_sub()[named_sub.first]);
167+
convert_from_json(named_sub.second, out.add(named_sub.first));
168168

169169
for(const auto &comment : in["comment"].object)
170-
convert_from_json(comment.second, out.get_comments()[comment.first]);
170+
convert_from_json(comment.second, out.add(comment.first));
171171
}

‎src/util/rename_symbol.cpp

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -133,6 +133,9 @@ Function: rename_symbolt::have_to_rename
133133

134134
bool rename_symbolt::have_to_rename(const exprt &dest) const
135135
{
136+
if(expr_map.empty() && type_map.empty())
137+
return false;
138+
136139
// first look at type
137140

138141
if(have_to_rename(dest.type()))
@@ -274,6 +277,9 @@ Function: rename_symbolt::have_to_rename
274277

275278
bool rename_symbolt::have_to_rename(const typet &dest) const
276279
{
280+
if(expr_map.empty() && type_map.empty())
281+
return false;
282+
277283
if(dest.has_subtype())
278284
if(have_to_rename(dest.subtype()))
279285
return true;

0 commit comments

Comments
 (0)