Skip to content

Commit 98f8962

Browse files
tautschnigtautschnig
committed
Various cleanup
1 parent ccd11f5 commit 98f8962

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

50 files changed

+222
-104
lines changed

‎src/ansi-c/ansi_c_entry_point.cpp

+2-4
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,7 @@ Author: Daniel Kroening, [email protected]
2222
exprt::operandst build_function_environment(
2323
const code_typet::parameterst &parameters,
2424
code_blockt &init_code,
25-
symbol_tablet &symbol_table,
26-
message_handlert &message_handler)
25+
symbol_tablet &symbol_table)
2726
{
2827
exprt::operandst main_arguments;
2928
main_arguments.resize(parameters.size());
@@ -432,8 +431,7 @@ bool generate_ansi_c_start_function(
432431
build_function_environment(
433432
parameters,
434433
init_code,
435-
symbol_table,
436-
message_handler);
434+
symbol_table);
437435
}
438436

439437
init_code.move_to_operands(call_main);

‎src/ansi-c/c_typecast.cpp

+8-3
Original file line numberDiff line numberDiff line change
@@ -277,7 +277,7 @@ typet c_typecastt::follow_with_qualifiers(const typet &src_type)
277277
c_typecastt::c_typet c_typecastt::get_c_type(
278278
const typet &type) const
279279
{
280-
unsigned width=type.get_int(ID_width);
280+
const std::size_t width = type.get_size_t(ID_width);
281281

282282
if(type.id()==ID_signedbv)
283283
{
@@ -396,8 +396,13 @@ void c_typecastt::implicit_typecast_arithmetic(
396396
case RATIONAL: new_type=rational_typet(); break;
397397
case REAL: new_type=real_typet(); break;
398398
case INTEGER: new_type=integer_typet(); break;
399-
case COMPLEX: return; // do nothing
400-
default: return;
399+
case COMPLEX:
400+
case OTHER:
401+
case VOIDPTR:
402+
case FIXEDBV:
403+
case LARGE_UNSIGNED_INT:
404+
case LARGE_SIGNED_INT:
405+
return; // do nothing
401406
}
402407

403408
if(new_type!=expr_type)

‎src/ansi-c/c_typecheck_code.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -563,7 +563,7 @@ void c_typecheck_baset::typecheck_gcc_switch_case_range(codet &code)
563563
implicit_typecast(code.op1(), switch_op_type);
564564
}
565565

566-
void c_typecheck_baset::typecheck_gcc_local_label(codet &code)
566+
void c_typecheck_baset::typecheck_gcc_local_label(codet &)
567567
{
568568
// these are just declarations, e.g.,
569569
// __label__ here, there;

‎src/ansi-c/c_typecheck_expr.cpp

+10-10
Original file line numberDiff line numberDiff line change
@@ -2694,20 +2694,20 @@ exprt c_typecheck_baset::do_special_functions(
26942694
// clang returns 4 for _Bool, gcc treats these as 'int'.
26952695
type_number =
26962696
config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::CLANG
2697-
? 4
2698-
: 1;
2697+
? 4u
2698+
: 1u;
26992699
}
27002700
else
27012701
{
27022702
type_number =
2703-
type.id() == ID_empty ? 0
2704-
: (type.id() == ID_bool || type.id() == ID_c_bool) ? 4
2705-
: (type.id() == ID_pointer || type.id() == ID_array) ? 5
2706-
: type.id() == ID_floatbv ? 8
2707-
: (type.id() == ID_complex && type.subtype().id() == ID_floatbv) ? 9
2708-
: type.id() == ID_struct ? 12
2709-
: type.id() == ID_union ? 13
2710-
: 1; // int, short, char, enum_tag
2703+
type.id() == ID_empty ? 0u
2704+
: (type.id() == ID_bool || type.id() == ID_c_bool) ? 4u
2705+
: (type.id() == ID_pointer || type.id() == ID_array) ? 5u
2706+
: type.id() == ID_floatbv ? 8u
2707+
: (type.id() == ID_complex && type.subtype().id() == ID_floatbv) ? 9u
2708+
: type.id() == ID_struct ? 12u
2709+
: type.id() == ID_union ? 13u
2710+
: 1u; // int, short, char, enum_tag
27112711
}
27122712

27132713
exprt tmp=from_integer(type_number, expr.type());

‎src/ansi-c/c_typecheck_type.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -1368,7 +1368,7 @@ void c_typecheck_baset::typecheck_c_bit_field_type(c_bit_field_typet &type)
13681368
throw 0;
13691369
}
13701370

1371-
sub_width=c_enum_type.subtype().get_int(ID_width);
1371+
sub_width = c_enum_type.subtype().get_size_t(ID_width);
13721372
}
13731373
else
13741374
{

‎src/ansi-c/expr2c.cpp

-23
Original file line numberDiff line numberDiff line change
@@ -1164,26 +1164,6 @@ std::string expr2ct::convert_unary(
11641164
return dest;
11651165
}
11661166

1167-
std::string expr2ct::convert_pointer_object_has_type(
1168-
const exprt &src,
1169-
unsigned precedence)
1170-
{
1171-
if(src.operands().size()!=1)
1172-
return convert_norep(src, precedence);
1173-
1174-
unsigned p0;
1175-
std::string op0=convert_with_precedence(src.op0(), p0);
1176-
1177-
std::string dest="POINTER_OBJECT_HAS_TYPE";
1178-
dest+='(';
1179-
dest+=op0;
1180-
dest+=", ";
1181-
dest+=convert(static_cast<const typet &>(src.find("object_type")));
1182-
dest+=')';
1183-
1184-
return dest;
1185-
}
1186-
11871167
std::string expr2ct::convert_allocate(const exprt &src, unsigned &precedence)
11881168
{
11891169
if(src.operands().size() != 2)
@@ -3578,9 +3558,6 @@ std::string expr2ct::convert_with_precedence(
35783558
else if(src.id()=="object_value")
35793559
return convert_function(src, "OBJECT_VALUE", precedence=16);
35803560

3581-
else if(src.id()=="pointer_object_has_type")
3582-
return convert_pointer_object_has_type(src, precedence=16);
3583-
35843561
else if(src.id()==ID_array_of)
35853562
return convert_array_of(src, precedence=16);
35863563

‎src/ansi-c/expr2c_class.h

-3
Original file line numberDiff line numberDiff line change
@@ -102,9 +102,6 @@ class expr2ct
102102
std::string convert_member(
103103
const member_exprt &src, unsigned precedence);
104104

105-
std::string convert_pointer_object_has_type(
106-
const exprt &src, unsigned precedence);
107-
108105
std::string convert_array_of(const exprt &src, unsigned precedence);
109106

110107
std::string convert_trinary(

‎src/ansi-c/padding.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -127,7 +127,7 @@ underlying_width(const c_bit_field_typet &type, const namespacet &ns)
127127
const typet &c_enum_type = ns.follow_tag(to_c_enum_tag_type(subtype));
128128

129129
if(c_enum_type.id() == ID_c_enum)
130-
return c_enum_type.subtype().get_int(ID_width);
130+
return c_enum_type.subtype().get_size_t(ID_width);
131131
else
132132
return {};
133133
}

‎src/config.inc

+5-1
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,11 @@ ifeq ($(BUILD_ENV),MSVC)
2121
# disable warning "behavior change ... called instead of ..."
2222
CXXFLAGS += /wd4350
2323
# disable warning "assignment operator could not be generated"
24-
CXXFLAGS += /wd4512
24+
CXXFLAGS += /wd4512 /wd4626
25+
# disable warning "copy constructor could not be generated"
26+
CXXFLAGS += /wd4625
27+
# disable warning "no override available, function is hidden"
28+
CXXFLAGS += /wd4266
2529
else
2630
CXXFLAGS += -Wall -pedantic -Werror -Wno-deprecated-declarations
2731
endif

‎src/goto-instrument/accelerate/overflow_instrumenter.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -110,8 +110,8 @@ void overflow_instrumentert::overflow_expr(
110110
}
111111

112112
const typet &old_type=ns.follow(expr.op0().type());
113-
std::size_t new_width=expr.type().get_int(ID_width);
114-
std::size_t old_width=old_type.get_int(ID_width);
113+
const std::size_t new_width = expr.type().get_size_t(ID_width);
114+
const std::size_t old_width = old_type.get_size_t(ID_width);
115115

116116
if(type.id()==ID_signedbv)
117117
{

‎src/jsil/jsil_typecheck.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -922,7 +922,7 @@ bool jsil_typecheck(
922922
bool jsil_typecheck(
923923
exprt &expr,
924924
message_handlert &message_handler,
925-
const namespacet &ns)
925+
const namespacet &)
926926
{
927927
const unsigned errors_before=
928928
message_handler.get_message_count(messaget::M_ERROR);
@@ -938,7 +938,7 @@ bool jsil_typecheck(
938938
jsil_typecheck.typecheck_expr(expr);
939939
}
940940

941-
catch(int e)
941+
catch(int)
942942
{
943943
jsil_typecheck.error();
944944
}

‎src/jsil/jsil_typecheck.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ class jsil_typecheckt:public typecheckt
5656

5757
void update_expr_type(exprt &expr, const typet &type);
5858
void make_type_compatible(exprt &expr, const typet &type, bool must);
59-
void typecheck_type_symbol(symbolt &symbol) {}
59+
void typecheck_type_symbol(symbolt &) {}
6060
void typecheck_non_type_symbol(symbolt &symbol);
6161
void typecheck_symbol_expr(symbol_exprt &symbol_expr);
6262
void typecheck_expr_side_effect_throw(side_effect_expr_throwt &expr);

‎src/langapi/language.cpp

+12-7
Original file line numberDiff line numberDiff line change
@@ -18,26 +18,26 @@ Author: Daniel Kroening, [email protected]
1818
#include <util/cprover_prefix.h>
1919
#include <util/std_types.h>
2020

21-
bool languaget::final(symbol_table_baset &symbol_table)
21+
bool languaget::final(symbol_table_baset &)
2222
{
2323
return false;
2424
}
2525

26-
bool languaget::interfaces(symbol_tablet &symbol_table)
26+
bool languaget::interfaces(symbol_tablet &)
2727
{
2828
return false;
2929
}
3030

3131
void languaget::dependencies(
32-
const std::string &module,
33-
std::set<std::string> &modules)
32+
const std::string &,
33+
std::set<std::string> &)
3434
{
3535
}
3636

3737
bool languaget::from_expr(
3838
const exprt &expr,
3939
std::string &code,
40-
const namespacet &ns)
40+
const namespacet &)
4141
{
4242
code=expr.pretty();
4343
return false;
@@ -46,7 +46,7 @@ bool languaget::from_expr(
4646
bool languaget::from_type(
4747
const typet &type,
4848
std::string &code,
49-
const namespacet &ns)
49+
const namespacet &)
5050
{
5151
code=type.pretty();
5252
return false;
@@ -55,7 +55,7 @@ bool languaget::from_type(
5555
bool languaget::type_to_name(
5656
const typet &type,
5757
std::string &name,
58-
const namespacet &ns)
58+
const namespacet &)
5959
{
6060
// probably ansi-c/type2name could be used as better fallback if moved to
6161
// util/
@@ -115,6 +115,8 @@ irep_idt languaget::generate_opaque_stub_body(
115115
symbolt &symbol,
116116
symbol_tablet &symbol_table)
117117
{
118+
(void)symbol;
119+
(void)symbol_table;
118120
return ID_nil;
119121
}
120122

@@ -131,6 +133,9 @@ parameter_symbolt languaget::build_stub_parameter_symbol(
131133
size_t parameter_index,
132134
const code_typet::parametert &parameter)
133135
{
136+
(void)function_symbol;
137+
(void)parameter_index;
138+
(void)parameter;
134139
error() << "language " << id()
135140
<< " doesn't implement build_stub_parameter_symbol. "
136141
<< "This means cannot use opaque functions." << eom;

‎src/langapi/language.h

+17-4
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,13 @@ class languaget:public messaget
4747
virtual bool preprocess(
4848
std::istream &instream,
4949
const std::string &path,
50-
std::ostream &outstream) { return false; }
50+
std::ostream &outstream)
51+
{
52+
(void)instream;
53+
(void)path;
54+
(void)outstream;
55+
return false;
56+
}
5157

5258
virtual bool parse(
5359
std::istream &instream,
@@ -73,18 +79,25 @@ class languaget:public messaget
7379
// add modules provided by currently parsed file to set
7480

7581
virtual void modules_provided(std::set<std::string> &modules)
76-
{ }
82+
{
83+
(void)modules;
84+
}
7785

7886
// add lazy functions provided to set
7987

8088
virtual void methods_provided(std::unordered_set<irep_idt> &methods) const
81-
{ }
89+
{
90+
(void)methods;
91+
}
8292

8393
// populate a lazy method
8494
virtual void
8595
convert_lazy_method(
8696
const irep_idt &function_id, symbol_table_baset &symbol_table)
87-
{ }
97+
{
98+
(void)function_id;
99+
(void)symbol_table;
100+
}
88101

89102
/// Final adjustments, e.g. initializing stub functions and globals that
90103
/// were discovered during function loading

‎src/langapi/language_ui.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -135,7 +135,7 @@ void language_uit::show_symbol_table(bool brief)
135135
show_symbol_table_xml_ui(brief);
136136
break;
137137

138-
default:
138+
case ui_message_handlert::uit::JSON_UI:
139139
error() << "cannot show symbol table in this format" << eom;
140140
}
141141
}

‎src/solvers/flattening/boolbv.h

+6
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,11 @@ class member_exprt;
3131
class boolbvt:public arrayst
3232
{
3333
public:
34+
#include <util/pragma_push.def>
35+
#ifdef _MSC_VER
36+
#pragma warning(disable:4355)
37+
// 'this' used in base member initializer list
38+
#endif
3439
boolbvt(
3540
const namespacet &_ns,
3641
propt &_prop):
@@ -42,6 +47,7 @@ class boolbvt:public arrayst
4247
map(_prop, _ns, boolbv_width)
4348
{
4449
}
50+
#include <util/pragma_pop.def>
4551

4652
virtual const bvt &convert_bv(const exprt &expr); // check cache
4753
virtual bvt convert_bitvector(const exprt &expr); // no cache

‎src/solvers/flattening/boolbv_not.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ bvt boolbvt::convert_not(const not_exprt &expr)
2323
{
2424
if((expr.type().id()==ID_verilog_signedbv ||
2525
expr.type().id()==ID_verilog_unsignedbv) &&
26-
expr.type().get_int(ID_width)==1)
26+
expr.type().get_size_t(ID_width) == 1)
2727
{
2828
literalt has_x_or_z=bv_utils.verilog_bv_has_x_or_z(op_bv);
2929
literalt normal_bits_zero=

‎src/solvers/flattening/boolbv_reduction.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -76,7 +76,7 @@ bvt boolbvt::convert_bv_reduction(const unary_exprt &expr)
7676
{
7777
if((expr.type().id()==ID_verilog_signedbv ||
7878
expr.type().id()==ID_verilog_unsignedbv) &&
79-
expr.type().get_int(ID_width)==1)
79+
expr.type().get_size_t(ID_width) == 1)
8080
{
8181
bvt bv;
8282
bv.resize(2);

‎src/solvers/prop/prop.h

+3-3
Original file line numberDiff line numberDiff line change
@@ -82,12 +82,12 @@ class propt:public messaget
8282
virtual bool cnf_handled_well() const { return true; }
8383

8484
// assumptions
85-
virtual void set_assumptions(const bvt &_assumptions) { }
85+
virtual void set_assumptions(const bvt &) { }
8686
virtual bool has_set_assumptions() const { return false; }
8787

8888
// variables
8989
virtual literalt new_variable()=0;
90-
virtual void set_variable_name(literalt a, const irep_idt &name) { }
90+
virtual void set_variable_name(literalt, const irep_idt &) { }
9191
virtual size_t no_variables() const=0;
9292
bvt new_variables(std::size_t width);
9393

@@ -111,7 +111,7 @@ class propt:public messaget
111111
virtual void set_frozen(literalt a) { }
112112

113113
// Resource limits:
114-
virtual void set_time_limit_seconds(uint32_t lim)
114+
virtual void set_time_limit_seconds(uint32_t)
115115
{
116116
warning() << "CPU limit ignored (not implemented)" << eom;
117117
}

‎src/solvers/refinement/string_builtin_function.h

+1
Original file line numberDiff line numberDiff line change
@@ -337,6 +337,7 @@ class string_builtin_function_with_no_evalt : public string_builtin_functiont
337337
// For now, there is no need for implementing that as `add_constraints`
338338
// should always be called on these functions
339339
UNIMPLEMENTED;
340+
return nil_exprt();
340341
}
341342
};
342343

0 commit comments

Comments
 (0)