Skip to content

Commit 8654b36

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 8654b36

File tree

6 files changed

+136
-178
lines changed

6 files changed

+136
-178
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: 59 additions & 88 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+
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;
@@ -340,7 +328,10 @@ void goto_convertt::remove_function_call(
340328
{
341329
if(!result_is_used)
342330
{
343-
assert(expr.operands().size()==2);
331+
DATA_INVARIANT(
332+
expr.operands().size() == 2,
333+
expr.find_source_location().as_string() +
334+
": function_call expects two operands");
344335
code_function_callt call(nil_exprt(), expr.op0(), expr.op1().operands());
345336
call.add_source_location()=expr.source_location();
346337
convert_function_call(call, dest, mode);
@@ -350,20 +341,14 @@ void goto_convertt::remove_function_call(
350341

351342
// get name of function, if available
352343

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-
}
344+
DATA_INVARIANT(
345+
expr.id() == ID_side_effect && expr.get(ID_statement) == ID_function_call,
346+
expr.find_source_location().as_string() + ": expected function call");
360347

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-
}
348+
DATA_INVARIANT(
349+
!expr.operands().empty(),
350+
expr.find_source_location().as_string() +
351+
": function_call expects at least one operand");
367352

368353
std::string new_base_name = "return_value";
369354
irep_idt new_symbol_mode = mode;
@@ -445,7 +430,7 @@ void goto_convertt::remove_cpp_delete(
445430
side_effect_exprt &expr,
446431
goto_programt &dest)
447432
{
448-
assert(expr.operands().size()==1);
433+
DATA_INVARIANT(expr.operands().size() == 1, "cpp_delete expected 1 operand");
449434

450435
codet tmp(expr.get_statement());
451436
tmp.add_source_location()=expr.source_location();
@@ -498,13 +483,10 @@ void goto_convertt::remove_temporary_object(
498483
goto_programt &dest)
499484
{
500485
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-
}
486+
DATA_INVARIANT(
487+
expr.operands().size() <= 1,
488+
expr.find_source_location().as_string() +
489+
": temporary_object takes 0 or 1 operands");
508490

509491
symbolt &new_symbol = new_tmp_symbol(
510492
expr.type(), "obj", dest, expr.find_source_location(), mode);
@@ -518,7 +500,10 @@ void goto_convertt::remove_temporary_object(
518500

519501
if(expr.find(ID_initializer).is_not_nil())
520502
{
521-
assert(expr.operands().empty());
503+
INVARIANT(
504+
expr.operands().empty(),
505+
expr.find_source_location().as_string() +
506+
": temporary_object takes 0 operands");
522507
exprt initializer=static_cast<const exprt &>(expr.find(ID_initializer));
523508
replace_new_object(new_symbol.symbol_expr(), initializer);
524509

@@ -539,19 +524,15 @@ void goto_convertt::remove_statement_expression(
539524
// The expression is copied into a temporary before the
540525
// scope is destroyed.
541526

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-
}
527+
DATA_INVARIANT(
528+
expr.operands().size() == 1,
529+
expr.find_source_location().as_string() +
530+
": statement_expression takes 1 operand");
548531

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-
}
532+
DATA_INVARIANT(
533+
expr.op0().id() == ID_code,
534+
expr.find_source_location().as_string() +
535+
": statement_expression takes code as operand");
555536

556537
codet &code=to_code(expr.op0());
557538

@@ -562,20 +543,15 @@ void goto_convertt::remove_statement_expression(
562543
return;
563544
}
564545

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-
}
546+
DATA_INVARIANT(
547+
code.get_statement() == ID_block,
548+
code.find_source_location().as_string() +
549+
": statement_expression takes block as operand");
571550

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-
}
551+
DATA_INVARIANT(
552+
!code.operands().empty(),
553+
expr.find_source_location().as_string() +
554+
": statement_expression takes non-empty block as operand");
579555

580556
// get last statement from block, following labels
581557
codet &last=to_code_block(code).find_last_statement();
@@ -604,10 +580,7 @@ void goto_convertt::remove_statement_expression(
604580
}
605581
else
606582
{
607-
error() << "statement_expression expects expression as "
608-
<< "last statement, but got `"
609-
<< last.get(ID_statement) << "'" << eom;
610-
throw 0;
583+
UNREACHABLE;
611584
}
612585

613586
{
@@ -683,8 +656,6 @@ void goto_convertt::remove_side_effect(
683656
}
684657
else
685658
{
686-
error().source_location=expr.find_source_location();
687-
error() << "cannot remove side effect (" << statement << ")" << eom;
688-
throw 0;
659+
UNREACHABLE;
689660
}
690661
}

0 commit comments

Comments
 (0)