Skip to content

Commit 6dcb6ab

Browse files
danpoedanpoe
committed
Error handling cleanup in src/util, for files with names starting with a-g
1 parent 8918ce9 commit 6dcb6ab

File tree

12 files changed

+142
-86
lines changed

12 files changed

+142
-86
lines changed

‎src/util/array_name.cpp‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -12,18 +12,19 @@ Author: Daniel Kroening, kroening@kroening.com
1212
#include "array_name.h"
1313

1414
#include "expr.h"
15+
#include "invariant.h"
1516
#include "namespace.h"
16-
#include "symbol.h"
1717
#include "ssa_expr.h"
18+
#include "symbol.h"
1819

1920
std::string array_name(
2021
const namespacet &ns,
2122
const exprt &expr)
2223
{
2324
if(expr.id()==ID_index)
2425
{
25-
if(expr.operands().size()!=2)
26-
throw "index takes two operands";
26+
DATA_INVARIANT(
27+
expr.operands().size() == 2, "index expression has two operands");
2728

2829
return array_name(ns, expr.op0())+"[]";
2930
}
@@ -44,7 +45,8 @@ std::string array_name(
4445
}
4546
else if(expr.id()==ID_member)
4647
{
47-
assert(expr.operands().size()==1);
48+
DATA_INVARIANT(
49+
expr.operands().size() == 1, "member expression has one operand");
4850
return array_name(ns, expr.op0())+"."+
4951
expr.get_string(ID_component_name);
5052
}

‎src/util/bv_arithmetic.cpp‎

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com
88

99
#include "bv_arithmetic.h"
1010

11-
#include <cassert>
1211
#include <ostream>
1312

1413
#include "string2int.h"
@@ -92,7 +91,7 @@ exprt bv_arithmetict::to_expr() const
9291

9392
bv_arithmetict &bv_arithmetict::operator/=(const bv_arithmetict &other)
9493
{
95-
assert(other.spec==spec);
94+
PRECONDITION(other.spec == spec);
9695

9796
if(other.value==0)
9897
value=0;
@@ -104,7 +103,7 @@ bv_arithmetict &bv_arithmetict::operator/=(const bv_arithmetict &other)
104103

105104
bv_arithmetict &bv_arithmetict::operator*=(const bv_arithmetict &other)
106105
{
107-
assert(other.spec==spec);
106+
PRECONDITION(other.spec == spec);
108107

109108
value*=other.value;
110109
adjust();
@@ -114,7 +113,7 @@ bv_arithmetict &bv_arithmetict::operator*=(const bv_arithmetict &other)
114113

115114
bv_arithmetict &bv_arithmetict::operator+=(const bv_arithmetict &other)
116115
{
117-
assert(other.spec==spec);
116+
PRECONDITION(other.spec == spec);
118117

119118
value+=other.value;
120119
adjust();
@@ -124,7 +123,7 @@ bv_arithmetict &bv_arithmetict::operator+=(const bv_arithmetict &other)
124123

125124
bv_arithmetict &bv_arithmetict::operator -= (const bv_arithmetict &other)
126125
{
127-
assert(other.spec==spec);
126+
PRECONDITION(other.spec == spec);
128127

129128
value-=other.value;
130129
adjust();
@@ -134,7 +133,7 @@ bv_arithmetict &bv_arithmetict::operator -= (const bv_arithmetict &other)
134133

135134
bv_arithmetict &bv_arithmetict::operator%=(const bv_arithmetict &other)
136135
{
137-
assert(other.spec==spec);
136+
PRECONDITION(other.spec == spec);
138137

139138
value%=other.value;
140139
adjust();
@@ -185,7 +184,7 @@ void bv_arithmetict::change_spec(const bv_spect &dest_spec)
185184

186185
void bv_arithmetict::from_expr(const exprt &expr)
187186
{
188-
assert(expr.is_constant());
187+
PRECONDITION(expr.is_constant());
189188
spec=bv_spect(expr.type());
190189
value=binary2integer(expr.get_string(ID_value), spec.is_signed);
191190
}

‎src/util/byte_operators.cpp‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com
88

99
#include "byte_operators.h"
1010

11-
#include <cassert>
12-
13-
#include "invariant.h"
1411
#include "config.h"
1512

1613
irep_idt byte_extract_id()

‎src/util/byte_operators.h‎

Lines changed: 37 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
1717
* \date Sun Jul 31 21:54:44 BST 2011
1818
*/
1919

20+
#include "invariant.h"
2021
#include "std_expr.h"
2122

2223
/*! \brief TO_BE_DOCUMENTED
@@ -51,13 +52,13 @@ class byte_extract_exprt:public binary_exprt
5152

5253
inline const byte_extract_exprt &to_byte_extract_expr(const exprt &expr)
5354
{
54-
assert(expr.operands().size()==2);
55+
PRECONDITION(expr.operands().size() == 2);
5556
return static_cast<const byte_extract_exprt &>(expr);
5657
}
5758

5859
inline byte_extract_exprt &to_byte_extract_expr(exprt &expr)
5960
{
60-
assert(expr.operands().size()==2);
61+
PRECONDITION(expr.operands().size() == 2);
6162
return static_cast<byte_extract_exprt &>(expr);
6263
}
6364

@@ -78,14 +79,20 @@ class byte_extract_little_endian_exprt:public byte_extract_exprt
7879
inline const byte_extract_little_endian_exprt
7980
&to_byte_extract_little_endian_expr(const exprt &expr)
8081
{
81-
assert(expr.id()==ID_byte_extract_little_endian && expr.operands().size()==2);
82+
PRECONDITION(expr.id() == ID_byte_extract_little_endian);
83+
DATA_INVARIANT(
84+
expr.operands().size() == 2, "byte extract expressions have two operands");
85+
8286
return static_cast<const byte_extract_little_endian_exprt &>(expr);
8387
}
8488

8589
inline byte_extract_little_endian_exprt
8690
&to_byte_extract_little_endian_expr(exprt &expr)
8791
{
88-
assert(expr.id()==ID_byte_extract_little_endian && expr.operands().size()==2);
92+
PRECONDITION(expr.id() == ID_byte_extract_little_endian);
93+
DATA_INVARIANT(
94+
expr.operands().size() == 2, "byte extract expressions have two operands");
95+
8996
return static_cast<byte_extract_little_endian_exprt &>(expr);
9097
}
9198

@@ -109,14 +116,20 @@ class byte_extract_big_endian_exprt:public byte_extract_exprt
109116
inline const byte_extract_big_endian_exprt
110117
&to_byte_extract_big_endian_expr(const exprt &expr)
111118
{
112-
assert(expr.id()==ID_byte_extract_big_endian && expr.operands().size()==2);
119+
PRECONDITION(expr.id() == ID_byte_extract_big_endian);
120+
DATA_INVARIANT(
121+
expr.operands().size() == 2, "byte extract expressions have two operands");
122+
113123
return static_cast<const byte_extract_big_endian_exprt &>(expr);
114124
}
115125

116126
inline byte_extract_big_endian_exprt
117127
&to_byte_extract_big_endian_expr(exprt &expr)
118128
{
119-
assert(expr.id()==ID_byte_extract_big_endian && expr.operands().size()==2);
129+
PRECONDITION(expr.id() == ID_byte_extract_big_endian);
130+
DATA_INVARIANT(
131+
expr.operands().size() == 2, "byte extract expressions have two operands");
132+
120133
return static_cast<byte_extract_big_endian_exprt &>(expr);
121134
}
122135

@@ -155,13 +168,13 @@ class byte_update_exprt:public exprt
155168

156169
inline const byte_update_exprt &to_byte_update_expr(const exprt &expr)
157170
{
158-
assert(expr.operands().size()==3);
171+
PRECONDITION(expr.operands().size() == 3);
159172
return static_cast<const byte_update_exprt &>(expr);
160173
}
161174

162175
inline byte_update_exprt &to_byte_update_expr(exprt &expr)
163176
{
164-
assert(expr.operands().size()==3);
177+
PRECONDITION(expr.operands().size() == 3);
165178
return static_cast<byte_update_exprt &>(expr);
166179
}
167180

@@ -185,14 +198,20 @@ class byte_update_little_endian_exprt:public byte_update_exprt
185198
inline const byte_update_little_endian_exprt
186199
&to_byte_update_little_endian_expr(const exprt &expr)
187200
{
188-
assert(expr.id()==ID_byte_update_little_endian && expr.operands().size()==3);
201+
PRECONDITION(expr.id() == ID_byte_update_little_endian);
202+
DATA_INVARIANT(
203+
expr.operands().size() == 3, "byte update expressions have three operands");
204+
189205
return static_cast<const byte_update_little_endian_exprt &>(expr);
190206
}
191207

192208
inline byte_update_little_endian_exprt
193209
&to_byte_update_little_endian_expr(exprt &expr)
194210
{
195-
assert(expr.id()==ID_byte_update_little_endian && expr.operands().size()==3);
211+
PRECONDITION(expr.id() == ID_byte_update_little_endian);
212+
DATA_INVARIANT(
213+
expr.operands().size() == 3, "byte update expressions have three operands");
214+
196215
return static_cast<byte_update_little_endian_exprt &>(expr);
197216
}
198217

@@ -216,14 +235,20 @@ class byte_update_big_endian_exprt:public byte_update_exprt
216235
inline const byte_update_big_endian_exprt
217236
&to_byte_update_big_endian_expr(const exprt &expr)
218237
{
219-
assert(expr.id()==ID_byte_update_big_endian && expr.operands().size()==3);
238+
PRECONDITION(expr.id() == ID_byte_update_big_endian);
239+
DATA_INVARIANT(
240+
expr.operands().size() == 3, "byte update expressions have three operands");
241+
220242
return static_cast<const byte_update_big_endian_exprt &>(expr);
221243
}
222244

223245
inline byte_update_big_endian_exprt
224246
&to_byte_update_big_endian_expr(exprt &expr)
225247
{
226-
assert(expr.id()==ID_byte_update_big_endian && expr.operands().size()==3);
248+
PRECONDITION(expr.id() == ID_byte_update_big_endian);
249+
DATA_INVARIANT(
250+
expr.operands().size() == 3, "byte update expressions have three operands");
251+
227252
return static_cast<byte_update_big_endian_exprt &>(expr);
228253
}
229254

‎src/util/config.cpp‎

Lines changed: 62 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -10,15 +10,16 @@ Author: Daniel Kroening, kroening@kroening.com
1010

1111
#include <cstdlib>
1212

13-
#include "namespace.h"
14-
#include "symbol_table.h"
1513
#include "arith_tools.h"
1614
#include "cmdline.h"
15+
#include "cprover_prefix.h"
16+
#include "exception_utils.h"
17+
#include "namespace.h"
1718
#include "simplify_expr.h"
1819
#include "std_expr.h"
19-
#include "cprover_prefix.h"
2020
#include "string2int.h"
2121
#include "string_utils.h"
22+
#include "symbol_table.h"
2223

2324
configt config;
2425

@@ -945,20 +946,42 @@ bool configt::set(const cmdlinet &cmdline)
945946
// the same architecture and OS that we are verifying for.
946947
if(arch==this_arch && os==this_os)
947948
{
948-
assert(ansi_c.int_width==sizeof(int)*8);
949-
assert(ansi_c.long_int_width==sizeof(long)*8);
950-
assert(ansi_c.bool_width==sizeof(bool)*8);
951-
assert(ansi_c.char_width==sizeof(char)*8);
952-
assert(ansi_c.short_int_width==sizeof(short)*8);
953-
assert(ansi_c.long_long_int_width==sizeof(long long)*8);
954-
assert(ansi_c.pointer_width==sizeof(void *)*8);
955-
assert(ansi_c.single_width==sizeof(float)*8);
956-
assert(ansi_c.double_width==sizeof(double)*8);
957-
assert(ansi_c.char_is_unsigned==(static_cast<char>(255)==255));
949+
INVARIANT(
950+
ansi_c.int_width == sizeof(int) * 8,
951+
"int width shall be equal to the system int width");
952+
INVARIANT(
953+
ansi_c.long_int_width == sizeof(long) * 8,
954+
"long int width shall be equal to the system long int width");
955+
INVARIANT(
956+
ansi_c.bool_width == sizeof(bool) * 8,
957+
"bool width shall be equal to the system bool width");
958+
INVARIANT(
959+
ansi_c.char_width == sizeof(char) * 8,
960+
"char width shall be equal to the system char width");
961+
INVARIANT(
962+
ansi_c.short_int_width == sizeof(short) * 8,
963+
"short int width shall be equal to the system short int width");
964+
INVARIANT(
965+
ansi_c.long_long_int_width == sizeof(long long) * 8,
966+
"long long int width shall be equal to the system long long int width");
967+
INVARIANT(
968+
ansi_c.pointer_width == sizeof(void *) * 8,
969+
"pointer width shall be equal to the system pointer width");
970+
INVARIANT(
971+
ansi_c.single_width == sizeof(float) * 8,
972+
"float width shall be equal to the system float width");
973+
INVARIANT(
974+
ansi_c.double_width == sizeof(double) * 8,
975+
"double width shall be equal to the system double width");
976+
INVARIANT(
977+
ansi_c.char_is_unsigned == (static_cast<char>(255) == 255),
978+
"char_is_unsigned flag shall indicate system char unsignedness");
958979

959980
#ifndef _WIN32
960981
// On Windows, long double width varies by compiler
961-
assert(ansi_c.long_double_width==sizeof(long double)*8);
982+
INVARIANT(
983+
ansi_c.long_double_width == sizeof(long double) * 8,
984+
"long double width shall be equal to the system long double width");
962985
#endif
963986
}
964987

@@ -1026,14 +1049,17 @@ bool configt::set(const cmdlinet &cmdline)
10261049
{
10271050
bv_encoding.object_bits=
10281051
unsafe_string2unsigned(cmdline.get_value("object-bits"));
1029-
bv_encoding.is_object_bits_default=false;
10301052

10311053
if(!(0<bv_encoding.object_bits &&
10321054
bv_encoding.object_bits<ansi_c.pointer_width))
10331055
{
1034-
throw "object-bits must be positive and less than the pointer width ("+
1035-
std::to_string(ansi_c.pointer_width)+") ";
1056+
throw invalid_user_input_exceptiont(
1057+
"object-bits must be positive and less than the pointer width (" +
1058+
std::to_string(ansi_c.pointer_width) + ") ",
1059+
"--object_bits");
10361060
}
1061+
1062+
bv_encoding.is_object_bits_default = false;
10371063
}
10381064

10391065
return false;
@@ -1069,21 +1095,17 @@ static irep_idt string_from_ns(
10691095
const irep_idt id=CPROVER_PREFIX "architecture_"+what;
10701096
const symbolt *symbol;
10711097

1072-
if(ns.lookup(id, symbol))
1073-
throw "failed to find "+id2string(id);
1098+
bool not_found = ns.lookup(id, symbol);
1099+
INVARIANT(!not_found, id2string(id) + " must be in namespace");
10741100

10751101
const exprt &tmp=symbol->value;
10761102

1077-
if(tmp.id()!=ID_address_of ||
1078-
tmp.operands().size()!=1 ||
1079-
tmp.op0().id()!=ID_index ||
1080-
tmp.op0().operands().size()!=2 ||
1081-
tmp.op0().op0().id()!=ID_string_constant)
1082-
{
1083-
throw
1084-
"symbol table configuration entry `"+id2string(id)+
1085-
"' is not a string constant";
1086-
}
1103+
INVARIANT(
1104+
tmp.id() == ID_address_of && tmp.operands().size() == 1 &&
1105+
tmp.op0().id() == ID_index && tmp.op0().operands().size() == 2 &&
1106+
tmp.op0().op0().id() == ID_string_constant,
1107+
"symbol table configuration entry `" + id2string(id) +
1108+
"' must be a string constant");
10871109

10881110
return tmp.op0().op0().get(ID_value);
10891111
}
@@ -1095,21 +1117,24 @@ static unsigned unsigned_from_ns(
10951117
const irep_idt id=CPROVER_PREFIX "architecture_"+what;
10961118
const symbolt *symbol;
10971119

1098-
if(ns.lookup(id, symbol))
1099-
throw "failed to find "+id2string(id);
1120+
bool not_found = ns.lookup(id, symbol);
1121+
INVARIANT(!not_found, id2string(id) + " must be in namespace");
11001122

11011123
exprt tmp=symbol->value;
11021124
simplify(tmp, ns);
11031125

1104-
if(tmp.id()!=ID_constant)
1105-
throw
1106-
"symbol table configuration entry `"+id2string(id)+"' is not a constant";
1126+
INVARIANT(
1127+
tmp.id() == ID_constant,
1128+
"symbol table configuration entry `" + id2string(id) +
1129+
"' must be a constant");
11071130

11081131
mp_integer int_value;
11091132

1110-
if(to_integer(to_constant_expr(tmp), int_value))
1111-
throw
1112-
"failed to convert symbol table configuration entry `"+id2string(id)+"'";
1133+
bool error = to_integer(to_constant_expr(tmp), int_value);
1134+
INVARIANT(
1135+
!error,
1136+
"symbol table configuration entry `" + id2string(id) +
1137+
"' must be convertible to mp_integer");
11131138

11141139
return integer2unsigned(int_value);
11151140
}

0 commit comments

Comments
 (0)