Skip to content

Commit d263ce7

Browse files
John NonweilerNlightNFotis
John Nonweiler
authored and
NlightNFotis
committed
Replace asserts and throws with INVARIANT etc.
1 parent 683efbc commit d263ce7

File tree

10 files changed

+41
-30
lines changed

10 files changed

+41
-30
lines changed

‎src/goto-symex/build_goto_trace.cpp‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,9 @@ exprt build_full_lhs_rec(
9292
id==ID_byte_extract_big_endian)
9393
{
9494
exprt tmp=src_original;
95-
assert(tmp.operands().size()==2);
95+
DATA_INVARIANT(
96+
tmp.operands().size() == 2,
97+
"byte_extract_exprt should have two operands.");
9698
tmp.op0()=build_full_lhs_rec(prop_conv, ns, tmp.op0(), src_ssa.op0());
9799

98100
// re-write into big case-split

‎src/goto-symex/goto_symex_state.cpp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -187,8 +187,8 @@ bool goto_symex_statet::constant_propagation_reference(const exprt &expr) const
187187
}
188188
else if(expr.id()==ID_member)
189189
{
190-
if(expr.operands().size()!=1)
191-
throw "member expects one operand";
190+
DATA_INVARIANT(
191+
expr.operands().size() == 1, "member_exprt takes one operand.");
192192

193193
return constant_propagation_reference(expr.op0());
194194
}

‎src/goto-symex/memory_model_pso.cpp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,8 +30,8 @@ bool memory_model_psot::program_order_is_relaxed(
3030
partial_order_concurrencyt::event_it e1,
3131
partial_order_concurrencyt::event_it e2) const
3232
{
33-
assert(e1->is_shared_read() || e1->is_shared_write());
34-
assert(e2->is_shared_read() || e2->is_shared_write());
33+
PRECONDITION(e1->is_shared_read() || e1->is_shared_write());
34+
PRECONDITION(e2->is_shared_read() || e2->is_shared_write());
3535

3636
// no po relaxation within atomic sections
3737
if(e1->atomic_section_id!=0 &&

‎src/goto-symex/memory_model_sc.cpp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -36,8 +36,8 @@ bool memory_model_sct::program_order_is_relaxed(
3636
partial_order_concurrencyt::event_it e1,
3737
partial_order_concurrencyt::event_it e2) const
3838
{
39-
assert(e1->is_shared_read() || e1->is_shared_write());
40-
assert(e2->is_shared_read() || e2->is_shared_write());
39+
PRECONDITION(e1->is_shared_read() || e1->is_shared_write());
40+
PRECONDITION(e2->is_shared_read() || e2->is_shared_write());
4141

4242
return false;
4343
}

‎src/goto-symex/memory_model_tso.cpp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -39,8 +39,8 @@ bool memory_model_tsot::program_order_is_relaxed(
3939
partial_order_concurrencyt::event_it e1,
4040
partial_order_concurrencyt::event_it e2) const
4141
{
42-
assert(e1->is_shared_read() || e1->is_shared_write());
43-
assert(e2->is_shared_read() || e2->is_shared_write());
42+
PRECONDITION(e1->is_shared_read() || e1->is_shared_write());
43+
PRECONDITION(e2->is_shared_read() || e2->is_shared_write());
4444

4545
// no po relaxation within atomic sections
4646
if(e1->atomic_section_id!=0 &&

‎src/goto-symex/partial_order_concurrency.cpp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -143,7 +143,7 @@ symbol_exprt partial_order_concurrencyt::clock(
143143
axiomt axiom)
144144
{
145145
irep_idt identifier;
146-
assert(!numbering.empty());
146+
PRECONDITION(!numbering.empty());
147147

148148
if(event->is_shared_write())
149149
identifier=rw_clock_id(event, axiom);
@@ -163,7 +163,7 @@ symbol_exprt partial_order_concurrencyt::clock(
163163

164164
void partial_order_concurrencyt::build_clock_type()
165165
{
166-
assert(!numbering.empty());
166+
PRECONDITION(!numbering.empty());
167167

168168
std::size_t width = address_bits(numbering.size());
169169
clock_type = unsignedbv_typet(width);

‎src/goto-symex/postcondition.cpp‎

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -76,20 +76,23 @@ bool postconditiont::is_used_address_of(
7676
}
7777
else if(expr.id()==ID_index)
7878
{
79-
assert(expr.operands().size()==2);
79+
DATA_INVARIANT(
80+
expr.operands().size() == 2, "index_exprt takes two operands.");
8081

8182
return
8283
is_used_address_of(expr.op0(), identifier) ||
8384
is_used(expr.op1(), identifier);
8485
}
8586
else if(expr.id()==ID_member)
8687
{
87-
assert(expr.operands().size()==1);
88+
DATA_INVARIANT(
89+
expr.operands().size() == 1, "member_exprt takes one operand.");
8890
return is_used_address_of(expr.op0(), identifier);
8991
}
9092
else if(expr.id()==ID_dereference)
9193
{
92-
assert(expr.operands().size()==1);
94+
DATA_INVARIANT(
95+
expr.operands().size() == 1, "dereference_exprt takes one operand.");
9396
return is_used(expr.op0(), identifier);
9497
}
9598

@@ -155,7 +158,8 @@ bool postconditiont::is_used(
155158
if(expr.id()==ID_address_of)
156159
{
157160
// only do index!
158-
assert(expr.operands().size()==1);
161+
DATA_INVARIANT(
162+
expr.operands().size() == 1, "address_of_exprt takes one operand.");
159163
return is_used_address_of(expr.op0(), identifier);
160164
}
161165
else if(expr.id()==ID_symbol &&
@@ -169,7 +173,8 @@ bool postconditiont::is_used(
169173
}
170174
else if(expr.id()==ID_dereference)
171175
{
172-
assert(expr.operands().size()==1);
176+
DATA_INVARIANT(
177+
expr.operands().size() == 1, "dereference_exprt takes one operand.");
173178

174179
// aliasing may happen here
175180

‎src/goto-symex/precondition.cpp‎

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -78,18 +78,21 @@ void preconditiont::compute_address_of(exprt &dest)
7878
}
7979
else if(dest.id()==ID_index)
8080
{
81-
assert(dest.operands().size()==2);
81+
DATA_INVARIANT(
82+
dest.operands().size() == 2, "index_exprt takes two operands.");
8283
compute_address_of(dest.op0());
8384
compute(dest.op1());
8485
}
8586
else if(dest.id()==ID_member)
8687
{
87-
assert(dest.operands().size()==1);
88+
DATA_INVARIANT(
89+
dest.operands().size() == 1, "member_exprt takes one operand.");
8890
compute_address_of(dest.op0());
8991
}
9092
else if(dest.id()==ID_dereference)
9193
{
92-
assert(dest.operands().size()==1);
94+
DATA_INVARIANT(
95+
dest.operands().size() == 1, "dereference_exprt takes one operand.");
9396
compute(dest.op0());
9497
}
9598
}
@@ -104,12 +107,14 @@ void preconditiont::compute_rec(exprt &dest)
104107
if(dest.id()==ID_address_of)
105108
{
106109
// only do index!
107-
assert(dest.operands().size()==1);
110+
DATA_INVARIANT(
111+
dest.operands().size() == 1, "address_of_exprt takes one operand.");
108112
compute_address_of(dest.op0());
109113
}
110114
else if(dest.id()==ID_dereference)
111115
{
112-
assert(dest.operands().size()==1);
116+
DATA_INVARIANT(
117+
dest.operands().size() == 1, "dereference_exprt takes one operand.");
113118

114119
const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
115120

‎src/goto-symex/slice.cpp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,7 @@ void symex_slicet::slice(symex_target_equationt::SSA_stept &SSA_step)
112112
void symex_slicet::slice_assignment(
113113
symex_target_equationt::SSA_stept &SSA_step)
114114
{
115-
assert(SSA_step.ssa_lhs.id()==ID_symbol);
115+
PRECONDITION(SSA_step.ssa_lhs.id() == ID_symbol);
116116
const irep_idt &id=SSA_step.ssa_lhs.get_identifier();
117117

118118
if(depends.find(id)==depends.end())
@@ -127,7 +127,7 @@ void symex_slicet::slice_assignment(
127127
void symex_slicet::slice_decl(
128128
symex_target_equationt::SSA_stept &SSA_step)
129129
{
130-
assert(SSA_step.ssa_lhs.id()==ID_symbol);
130+
PRECONDITION(SSA_step.ssa_lhs.id() == ID_symbol);
131131
const irep_idt &id=SSA_step.ssa_lhs.get_identifier();
132132

133133
if(depends.find(id)==depends.end())

‎src/goto-symex/symex_assign.cpp‎

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,7 @@ exprt goto_symext::add_to_lhs(
9191
const exprt &lhs,
9292
const exprt &what)
9393
{
94-
assert(lhs.id()!=ID_symbol);
94+
PRECONDITION(lhs.id() != ID_symbol);
9595
exprt tmp_what=what;
9696

9797
if(tmp_what.id()!=ID_symbol)
@@ -170,8 +170,8 @@ void goto_symext::symex_assign_rec(
170170
}
171171
else if(lhs.id() == ID_complex_real)
172172
{
173+
// this is stuff like __real__ x = 1;
173174
const complex_real_exprt &complex_real_expr = to_complex_real_expr(lhs);
174-
175175
const complex_imag_exprt complex_imag_expr(complex_real_expr.op());
176176

177177
complex_exprt new_rhs(
@@ -284,7 +284,7 @@ void goto_symext::symex_assign_typecast(
284284
{
285285
// these may come from dereferencing on the lhs
286286

287-
assert(lhs.operands().size()==1);
287+
PRECONDITION(lhs.operands().size() == 1);
288288

289289
exprt rhs_typecasted=rhs;
290290
rhs_typecasted.make_typecast(lhs.op0().type());
@@ -306,9 +306,7 @@ void goto_symext::symex_assign_array(
306306
// lhs must be index operand
307307
// that takes two operands: the first must be an array
308308
// the second is the index
309-
310-
if(lhs.operands().size()!=2)
311-
throw "index must have two operands";
309+
DATA_INVARIANT(lhs.operands().size() == 2, "index_exprt takes two operands");
312310

313311
const exprt &lhs_array=lhs.array();
314312
const exprt &lhs_index=lhs.index();
@@ -369,7 +367,8 @@ void goto_symext::symex_assign_struct_member(
369367
// typecasts involved? C++ does that for inheritance.
370368
if(lhs_struct.id()==ID_typecast)
371369
{
372-
assert(lhs_struct.operands().size()==1);
370+
DATA_INVARIANT(
371+
lhs_struct.operands().size() == 1, "typecast_exprt takes one operand.");
373372

374373
if(lhs_struct.op0().id() == ID_null_object)
375374
{

0 commit comments

Comments
 (0)