Skip to content

Commit 57a04a7

Browse files
Andreas PaschosNlightNFotis
Andreas Paschos
authored and
NlightNFotis
committed
Convert asserts and throws to INVARIANTs for files starting with g
1 parent d73d2db commit 57a04a7

File tree

6 files changed

+147
-191
lines changed

6 files changed

+147
-191
lines changed

‎src/goto-programs/goto_convert_exceptions.cpp‎

Lines changed: 23 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -18,12 +18,10 @@ void goto_convertt::convert_msc_try_finally(
1818
goto_programt &dest,
1919
const irep_idt &mode)
2020
{
21-
if(code.operands().size()!=2)
22-
{
23-
error().source_location=code.find_source_location();
24-
error() << "msc_try_finally expects two arguments" << eom;
25-
throw 0;
26-
}
21+
DATA_INVARIANT(
22+
code.operands().size() == 2,
23+
code.find_source_location().as_string() +
24+
": msc_try_finally expects two arguments");
2725

2826
goto_programt tmp;
2927
tmp.add_instruction(SKIP)->source_location=code.source_location();
@@ -57,12 +55,10 @@ void goto_convertt::convert_msc_try_except(
5755
goto_programt &dest,
5856
const irep_idt &mode)
5957
{
60-
if(code.operands().size()!=3)
61-
{
62-
error().source_location=code.find_source_location();
63-
error() << "msc_try_except expects three arguments" << eom;
64-
throw 0;
65-
}
58+
DATA_INVARIANT(
59+
code.operands().size() == 3,
60+
code.find_source_location().as_string() +
61+
": msc_try_except expects three arguments");
6662

6763
convert(to_code(code.op0()), dest, mode);
6864

@@ -74,12 +70,9 @@ void goto_convertt::convert_msc_leave(
7470
goto_programt &dest,
7571
const irep_idt &mode)
7672
{
77-
if(!targets.leave_set)
78-
{
79-
error().source_location=code.find_source_location();
80-
error() << "leave without target" << eom;
81-
throw 0;
82-
}
73+
DATA_INVARIANT(
74+
targets.leave_set,
75+
code.find_source_location().as_string() + ": leave without target");
8376

8477
// need to process destructor stack
8578
for(std::size_t d=targets.destructor_stack.size();
@@ -101,7 +94,10 @@ void goto_convertt::convert_try_catch(
10194
goto_programt &dest,
10295
const irep_idt &mode)
10396
{
104-
assert(code.operands().size()>=2);
97+
DATA_INVARIANT(
98+
code.operands().size() >= 2,
99+
code.find_source_location().as_string() +
100+
": try_catch expects at least two arguments");
105101

106102
// add the CATCH-push instruction to 'dest'
107103
goto_programt::targett catch_push_instruction=dest.add_instruction();
@@ -159,12 +155,10 @@ void goto_convertt::convert_CPROVER_try_catch(
159155
goto_programt &dest,
160156
const irep_idt &mode)
161157
{
162-
if(code.operands().size()!=2)
163-
{
164-
error().source_location=code.find_source_location();
165-
error() << "CPROVER_try_catch expects two arguments" << eom;
166-
throw 0;
167-
}
158+
DATA_INVARIANT(
159+
code.operands().size() == 2,
160+
code.find_source_location().as_string() +
161+
": CPROVER_try_catch expects two arguments");
168162

169163
// this is where we go after 'throw'
170164
goto_programt tmp;
@@ -235,12 +229,10 @@ void goto_convertt::convert_CPROVER_try_finally(
235229
goto_programt &dest,
236230
const irep_idt &mode)
237231
{
238-
if(code.operands().size()!=2)
239-
{
240-
error().source_location=code.find_source_location();
241-
error() << "CPROVER_try_finally expects two arguments" << eom;
242-
throw 0;
243-
}
232+
DATA_INVARIANT(
233+
code.operands().size() == 2,
234+
code.find_source_location().as_string() +
235+
": CPROVER_try_finally expects two arguments");
244236

245237
// first put 'finally' code onto destructor stack
246238
targets.destructor_stack.push_back(to_code(code.op1()));

‎src/goto-programs/goto_convert_side_effect.cpp‎

Lines changed: 58 additions & 90 deletions
Original file line numberDiff line numberDiff line change
@@ -60,12 +60,10 @@ void goto_convertt::remove_assignment(
6060
statement==ID_assign_bitxor ||
6161
statement==ID_assign_bitor)
6262
{
63-
if(expr.operands().size()!=2)
64-
{
65-
error().source_location=expr.find_source_location();
66-
error() << statement << " takes two arguments" << eom;
67-
throw 0;
68-
}
63+
DATA_INVARIANT(
64+
expr.operands().size() == 2,
65+
expr.find_source_location().as_string() + ": " + id2string(statement) +
66+
" takes two arguments");
6967

7068
irep_idt new_id;
7169

@@ -93,10 +91,7 @@ void goto_convertt::remove_assignment(
9391
new_id=ID_bitor;
9492
else
9593
{
96-
error().source_location=expr.find_source_location();
97-
error() << "assignment `" << statement << "' not yet supported"
98-
<< eom;
99-
throw 0;
94+
UNREACHABLE;
10095
}
10196

10297
exprt rhs;
@@ -143,17 +138,16 @@ void goto_convertt::remove_pre(
143138
bool result_is_used,
144139
const irep_idt &mode)
145140
{
146-
if(expr.operands().size()!=1)
147-
{
148-
error().source_location=expr.find_source_location();
149-
error() << "preincrement/predecrement must have one operand" << eom;
150-
throw 0;
151-
}
141+
DATA_INVARIANT(
142+
expr.operands().size() == 1,
143+
expr.find_source_location().as_string() +
144+
": preincrement/predecrement must have one operand");
152145

153146
const irep_idt statement=expr.get_statement();
154147

155-
assert(statement==ID_preincrement ||
156-
statement==ID_predecrement);
148+
DATA_INVARIANT(
149+
statement == ID_preincrement || statement == ID_predecrement,
150+
"expected preincrement or predecrement");
157151

158152
exprt rhs;
159153
rhs.add_source_location()=expr.source_location();
@@ -198,9 +192,7 @@ void goto_convertt::remove_pre(
198192
constant_type=op_type;
199193
else
200194
{
201-
error().source_location=expr.find_source_location();
202-
error() << "no constant one of type " << op_type.pretty() << eom;
203-
throw 0;
195+
UNREACHABLE;
204196
}
205197

206198
exprt constant=from_integer(1, constant_type);
@@ -235,18 +227,16 @@ void goto_convertt::remove_post(
235227

236228
// we have ...(op++)...
237229

238-
if(expr.operands().size()!=1)
239-
{
240-
error().source_location=expr.find_source_location();
241-
error() << "postincrement/postdecrement must have one operand"
242-
<< eom;
243-
throw 0;
244-
}
230+
DATA_INVARIANT(
231+
expr.operands().size() == 1,
232+
expr.find_source_location().as_string() +
233+
": postincrement/postdecrement must have one operand");
245234

246235
const irep_idt statement=expr.get_statement();
247236

248-
assert(statement==ID_postincrement ||
249-
statement==ID_postdecrement);
237+
DATA_INVARIANT(
238+
statement == ID_postincrement || statement == ID_postdecrement,
239+
"expected postincrement or postdecrement");
250240

251241
exprt rhs;
252242
rhs.add_source_location()=expr.source_location();
@@ -291,9 +281,7 @@ void goto_convertt::remove_post(
291281
constant_type=op_type;
292282
else
293283
{
294-
error().source_location=expr.find_source_location();
295-
error() << "no constant one of type " << op_type.pretty() << eom;
296-
throw 0;
284+
UNREACHABLE;
297285
}
298286

299287
exprt constant;
@@ -338,9 +326,13 @@ void goto_convertt::remove_function_call(
338326
const irep_idt &mode,
339327
bool result_is_used)
340328
{
329+
DATA_INVARIANT(
330+
expr.operands().size() == 2,
331+
expr.find_source_location().as_string() +
332+
": function_call expects two operands");
333+
341334
if(!result_is_used)
342335
{
343-
assert(expr.operands().size()==2);
344336
code_function_callt call(nil_exprt(), expr.op0(), expr.op1().operands());
345337
call.add_source_location()=expr.source_location();
346338
convert_function_call(call, dest, mode);
@@ -350,20 +342,9 @@ void goto_convertt::remove_function_call(
350342

351343
// get name of function, if available
352344

353-
if(expr.id()!=ID_side_effect ||
354-
expr.get(ID_statement)!=ID_function_call)
355-
{
356-
error().source_location=expr.find_source_location();
357-
error() << "expected function call" << eom;
358-
throw 0;
359-
}
360-
361-
if(expr.operands().empty())
362-
{
363-
error().source_location=expr.find_source_location();
364-
error() << "function_call expects at least one operand" << eom;
365-
throw 0;
366-
}
345+
DATA_INVARIANT(
346+
expr.id() == ID_side_effect && expr.get(ID_statement) == ID_function_call,
347+
expr.find_source_location().as_string() + ": expected function call");
367348

368349
std::string new_base_name = "return_value";
369350
irep_idt new_symbol_mode = mode;
@@ -445,7 +426,8 @@ void goto_convertt::remove_cpp_delete(
445426
side_effect_exprt &expr,
446427
goto_programt &dest)
447428
{
448-
assert(expr.operands().size()==1);
429+
DATA_INVARIANT(expr.operands().size() == 1,
430+
"cpp_delete expected one operand");
449431

450432
codet tmp(expr.get_statement());
451433
tmp.add_source_location()=expr.source_location();
@@ -498,13 +480,10 @@ void goto_convertt::remove_temporary_object(
498480
goto_programt &dest)
499481
{
500482
const irep_idt &mode = expr.get(ID_mode);
501-
if(expr.operands().size()!=1 &&
502-
!expr.operands().empty())
503-
{
504-
error().source_location=expr.find_source_location();
505-
error() << "temporary_object takes 0 or 1 operands" << eom;
506-
throw 0;
507-
}
483+
DATA_INVARIANT(
484+
expr.operands().size() <= 1,
485+
expr.find_source_location().as_string() +
486+
": temporary_object takes zero or one operands");
508487

509488
symbolt &new_symbol = new_tmp_symbol(
510489
expr.type(), "obj", dest, expr.find_source_location(), mode);
@@ -518,7 +497,10 @@ void goto_convertt::remove_temporary_object(
518497

519498
if(expr.find(ID_initializer).is_not_nil())
520499
{
521-
assert(expr.operands().empty());
500+
INVARIANT(
501+
expr.operands().empty(),
502+
expr.find_source_location().as_string() +
503+
": temporary_object takes zero operands");
522504
exprt initializer=static_cast<const exprt &>(expr.find(ID_initializer));
523505
replace_new_object(new_symbol.symbol_expr(), initializer);
524506

@@ -539,19 +521,15 @@ void goto_convertt::remove_statement_expression(
539521
// The expression is copied into a temporary before the
540522
// scope is destroyed.
541523

542-
if(expr.operands().size()!=1)
543-
{
544-
error().source_location=expr.find_source_location();
545-
error() << "statement_expression takes 1 operand" << eom;
546-
throw 0;
547-
}
524+
DATA_INVARIANT(
525+
expr.operands().size() == 1,
526+
expr.find_source_location().as_string() +
527+
": statement_expression takes one operand");
548528

549-
if(expr.op0().id()!=ID_code)
550-
{
551-
error().source_location=expr.op0().find_source_location();
552-
error() << "statement_expression takes code as operand" << eom;
553-
throw 0;
554-
}
529+
DATA_INVARIANT(
530+
expr.op0().id() == ID_code,
531+
expr.find_source_location().as_string() +
532+
": statement_expression takes code as operand");
555533

556534
codet &code=to_code(expr.op0());
557535

@@ -562,20 +540,15 @@ void goto_convertt::remove_statement_expression(
562540
return;
563541
}
564542

565-
if(code.get_statement()!=ID_block)
566-
{
567-
error().source_location=code.find_source_location();
568-
error() << "statement_expression takes block as operand" << eom;
569-
throw 0;
570-
}
543+
DATA_INVARIANT(
544+
code.get_statement() == ID_block,
545+
code.find_source_location().as_string() +
546+
": statement_expression takes block as operand");
571547

572-
if(code.operands().empty())
573-
{
574-
error().source_location=expr.find_source_location();
575-
error() << "statement_expression takes non-empty block as operand"
576-
<< eom;
577-
throw 0;
578-
}
548+
DATA_INVARIANT(
549+
!code.operands().empty(),
550+
expr.find_source_location().as_string() +
551+
": statement_expression takes non-empty block as operand");
579552

580553
// get last statement from block, following labels
581554
codet &last=to_code_block(code).find_last_statement();
@@ -588,7 +561,7 @@ void goto_convertt::remove_statement_expression(
588561
symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type);
589562
tmp_symbol_expr.add_source_location()=source_location;
590563

591-
if(last.get(ID_statement)==ID_expression)
564+
if(last.get(ID_statement_expressionement)==ID_expression)
592565
{
593566
// we turn this into an assignment
594567
exprt e=to_code_expression(last).expression();
@@ -604,10 +577,7 @@ void goto_convertt::remove_statement_expression(
604577
}
605578
else
606579
{
607-
error() << "statement_expression expects expression as "
608-
<< "last statement, but got `"
609-
<< last.get(ID_statement) << "'" << eom;
610-
throw 0;
580+
UNREACHABLE;
611581
}
612582

613583
{
@@ -683,8 +653,6 @@ void goto_convertt::remove_side_effect(
683653
}
684654
else
685655
{
686-
error().source_location=expr.find_source_location();
687-
error() << "cannot remove side effect (" << statement << ")" << eom;
688-
throw 0;
656+
UNREACHABLE;
689657
}
690658
}

0 commit comments

Comments
 (0)