Skip to content

Commit 5b5ba13

Browse files
tautschnigtautschnig
authored
Merge pull request #2762 from danpoe/refactor/error-handling-util
Error handling cleanup in src/util (files starting with a-g)
2 parents 070da7b + 756c0b9 commit 5b5ba13

16 files changed

+194
-151
lines changed

‎src/ansi-c/ansi_c_entry_point.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -177,8 +177,7 @@ bool ansi_c_entry_point(
177177
return false; // give up
178178
}
179179

180-
if(static_lifetime_init(symbol_table, symbol.location, message_handler))
181-
return true;
180+
static_lifetime_init(symbol_table, symbol.location, message_handler);
182181

183182
return generate_ansi_c_start_function(symbol, symbol_table, message_handler);
184183
}

‎src/linking/static_lifetime_init.cpp

Lines changed: 9 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -22,17 +22,16 @@ Author: Daniel Kroening, [email protected]
2222

2323
#include <goto-programs/goto_functions.h>
2424

25-
bool static_lifetime_init(
25+
void static_lifetime_init(
2626
symbol_tablet &symbol_table,
2727
const source_locationt &source_location,
2828
message_handlert &message_handler)
2929
{
30-
namespacet ns(symbol_table);
30+
PRECONDITION(symbol_table.has_symbol(INITIALIZE_FUNCTION));
3131

32-
const auto maybe_symbol=symbol_table.get_writeable(INITIALIZE_FUNCTION);
33-
if(!maybe_symbol)
34-
return false;
35-
symbolt &init_symbol=*maybe_symbol;
32+
const namespacet ns(symbol_table);
33+
34+
symbolt &init_symbol = symbol_table.get_writeable_ref(INITIALIZE_FUNCTION);
3635

3736
init_symbol.value=code_blockt();
3837
init_symbol.value.add_source_location()=source_location;
@@ -117,16 +116,10 @@ bool static_lifetime_init(
117116

118117
if(symbol.value.is_nil())
119118
{
120-
try
121-
{
122-
namespacet ns(symbol_table);
123-
rhs=zero_initializer(symbol.type, symbol.location, ns, message_handler);
124-
assert(rhs.is_not_nil());
125-
}
126-
catch(...)
127-
{
128-
return true;
129-
}
119+
const namespacet ns(symbol_table);
120+
rhs = zero_initializer(symbol.type, symbol.location, ns, message_handler);
121+
INVARIANT(
122+
rhs.is_not_nil(), "result of zero-initialization must be non-nil");
130123
}
131124
else
132125
rhs=symbol.value;
@@ -156,6 +149,4 @@ bool static_lifetime_init(
156149
dest.move_to_operands(function_call);
157150
}
158151
}
159-
160-
return false;
161152
}

‎src/linking/static_lifetime_init.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ class message_handlert;
1616
class source_locationt;
1717
class symbol_tablet;
1818

19-
bool static_lifetime_init(
19+
void static_lifetime_init(
2020
symbol_tablet &symbol_table,
2121
const source_locationt &source_location,
2222
message_handlert &message_handler);

‎src/util/array_name.cpp

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -12,20 +12,18 @@ Author: Daniel Kroening, [email protected]
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";
27-
28-
return array_name(ns, expr.op0())+"[]";
26+
return array_name(ns, to_index_expr(expr).array()) + "[]";
2927
}
3028
else if(is_ssa_expr(expr))
3129
{
@@ -44,9 +42,10 @@ std::string array_name(
4442
}
4543
else if(expr.id()==ID_member)
4644
{
47-
assert(expr.operands().size()==1);
48-
return array_name(ns, expr.op0())+"."+
49-
expr.get_string(ID_component_name);
45+
const member_exprt &member_expr = to_member_expr(expr);
46+
47+
return array_name(ns, member_expr.compound()) + "." +
48+
id2string(member_expr.get_component_name());
5049
}
5150

5251
return "array";

‎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, [email protected]
88

99
#include "bv_arithmetic.h"
1010

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

1413
#include "string2int.h"
@@ -90,7 +89,7 @@ exprt bv_arithmetict::to_expr() const
9089

9190
bv_arithmetict &bv_arithmetict::operator/=(const bv_arithmetict &other)
9291
{
93-
assert(other.spec==spec);
92+
PRECONDITION(other.spec == spec);
9493

9594
if(other.value==0)
9695
value=0;
@@ -102,7 +101,7 @@ bv_arithmetict &bv_arithmetict::operator/=(const bv_arithmetict &other)
102101

103102
bv_arithmetict &bv_arithmetict::operator*=(const bv_arithmetict &other)
104103
{
105-
assert(other.spec==spec);
104+
PRECONDITION(other.spec == spec);
106105

107106
value*=other.value;
108107
adjust();
@@ -112,7 +111,7 @@ bv_arithmetict &bv_arithmetict::operator*=(const bv_arithmetict &other)
112111

113112
bv_arithmetict &bv_arithmetict::operator+=(const bv_arithmetict &other)
114113
{
115-
assert(other.spec==spec);
114+
PRECONDITION(other.spec == spec);
116115

117116
value+=other.value;
118117
adjust();
@@ -122,7 +121,7 @@ bv_arithmetict &bv_arithmetict::operator+=(const bv_arithmetict &other)
122121

123122
bv_arithmetict &bv_arithmetict::operator -= (const bv_arithmetict &other)
124123
{
125-
assert(other.spec==spec);
124+
PRECONDITION(other.spec == spec);
126125

127126
value-=other.value;
128127
adjust();
@@ -132,7 +131,7 @@ bv_arithmetict &bv_arithmetict::operator -= (const bv_arithmetict &other)
132131

133132
bv_arithmetict &bv_arithmetict::operator%=(const bv_arithmetict &other)
134133
{
135-
assert(other.spec==spec);
134+
PRECONDITION(other.spec == spec);
136135

137136
value%=other.value;
138137
adjust();
@@ -183,7 +182,7 @@ void bv_arithmetict::change_spec(const bv_spect &dest_spec)
183182

184183
void bv_arithmetict::from_expr(const exprt &expr)
185184
{
186-
assert(expr.is_constant());
185+
PRECONDITION(expr.is_constant());
187186
spec=bv_spect(expr.type());
188187
value=binary2integer(expr.get_string(ID_value), spec.is_signed);
189188
}

‎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, [email protected]
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, [email protected]
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

@@ -154,13 +167,13 @@ class byte_update_exprt : public ternary_exprt
154167

155168
inline const byte_update_exprt &to_byte_update_expr(const exprt &expr)
156169
{
157-
assert(expr.operands().size()==3);
170+
PRECONDITION(expr.operands().size() == 3);
158171
return static_cast<const byte_update_exprt &>(expr);
159172
}
160173

161174
inline byte_update_exprt &to_byte_update_expr(exprt &expr)
162175
{
163-
assert(expr.operands().size()==3);
176+
PRECONDITION(expr.operands().size() == 3);
164177
return static_cast<byte_update_exprt &>(expr);
165178
}
166179

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

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

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

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

0 commit comments

Comments
 (0)