Skip to content

Commit a04da2e

Browse files
NlightNFotisNlightNFotis
authored
Merge pull request #2904 from NlightNFotis/2836_takeover
Cleanup of error handling of some of the files under goto-programs
2 parents 683efbc + c952f55 commit a04da2e

6 files changed

+145
-190
lines changed

‎src/goto-programs/goto_convert_exceptions.cpp

Lines changed: 22 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+
INVARIANT_WITH_DIAGNOSTICS(
22+
code.operands().size() == 2,
23+
"msc_try_finally expects two arguments",
24+
code.find_source_location());
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+
INVARIANT_WITH_DIAGNOSTICS(
59+
code.operands().size() == 3,
60+
"msc_try_except expects three arguments",
61+
code.find_source_location());
6662

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

@@ -74,12 +70,8 @@ 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+
INVARIANT_WITH_DIAGNOSTICS(
74+
targets.leave_set, "leave without target", code.find_source_location());
8375

8476
// need to process destructor stack
8577
for(std::size_t d=targets.destructor_stack.size();
@@ -101,7 +93,10 @@ void goto_convertt::convert_try_catch(
10193
goto_programt &dest,
10294
const irep_idt &mode)
10395
{
104-
assert(code.operands().size()>=2);
96+
INVARIANT_WITH_DIAGNOSTICS(
97+
code.operands().size() >= 2,
98+
"try_catch expects at least two arguments",
99+
code.find_source_location());
105100

106101
// add the CATCH-push instruction to 'dest'
107102
goto_programt::targett catch_push_instruction=dest.add_instruction();
@@ -159,12 +154,10 @@ void goto_convertt::convert_CPROVER_try_catch(
159154
goto_programt &dest,
160155
const irep_idt &mode)
161156
{
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-
}
157+
INVARIANT_WITH_DIAGNOSTICS(
158+
code.operands().size() == 2,
159+
"CPROVER_try_catch expects two arguments",
160+
code.find_source_location());
168161

169162
// this is where we go after 'throw'
170163
goto_programt tmp;
@@ -235,12 +228,10 @@ void goto_convertt::convert_CPROVER_try_finally(
235228
goto_programt &dest,
236229
const irep_idt &mode)
237230
{
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-
}
231+
INVARIANT_WITH_DIAGNOSTICS(
232+
code.operands().size() == 2,
233+
"CPROVER_try_finally expects two arguments",
234+
code.find_source_location());
244235

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

‎src/goto-programs/goto_convert_side_effect.cpp

Lines changed: 57 additions & 89 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_WITH_DIAGNOSTICS(
64+
expr.operands().size() == 2,
65+
id2string(statement) + " expects two arguments",
66+
expr.find_source_location());
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;
@@ -154,17 +149,16 @@ void goto_convertt::remove_pre(
154149
bool result_is_used,
155150
const irep_idt &mode)
156151
{
157-
if(expr.operands().size()!=1)
158-
{
159-
error().source_location=expr.find_source_location();
160-
error() << "preincrement/predecrement must have one operand" << eom;
161-
throw 0;
162-
}
152+
INVARIANT_WITH_DIAGNOSTICS(
153+
expr.operands().size() == 1,
154+
"preincrement/predecrement must have one operand",
155+
expr.find_source_location());
163156

164157
const irep_idt statement=expr.get_statement();
165158

166-
assert(statement==ID_preincrement ||
167-
statement==ID_predecrement);
159+
DATA_INVARIANT(
160+
statement == ID_preincrement || statement == ID_predecrement,
161+
"expects preincrement or predecrement");
168162

169163
exprt rhs;
170164
rhs.add_source_location()=expr.source_location();
@@ -209,9 +203,7 @@ void goto_convertt::remove_pre(
209203
constant_type=op_type;
210204
else
211205
{
212-
error().source_location=expr.find_source_location();
213-
error() << "no constant one of type " << op_type.pretty() << eom;
214-
throw 0;
206+
UNREACHABLE;
215207
}
216208

217209
exprt constant=from_integer(1, constant_type);
@@ -246,18 +238,16 @@ void goto_convertt::remove_post(
246238

247239
// we have ...(op++)...
248240

249-
if(expr.operands().size()!=1)
250-
{
251-
error().source_location=expr.find_source_location();
252-
error() << "postincrement/postdecrement must have one operand"
253-
<< eom;
254-
throw 0;
255-
}
241+
INVARIANT_WITH_DIAGNOSTICS(
242+
expr.operands().size() == 1,
243+
"postincrement/postdecrement must have one operand",
244+
expr.find_source_location());
256245

257246
const irep_idt statement=expr.get_statement();
258247

259-
assert(statement==ID_postincrement ||
260-
statement==ID_postdecrement);
248+
DATA_INVARIANT(
249+
statement == ID_postincrement || statement == ID_postdecrement,
250+
"expects postincrement or postdecrement");
261251

262252
exprt rhs;
263253
rhs.add_source_location()=expr.source_location();
@@ -302,9 +292,7 @@ void goto_convertt::remove_post(
302292
constant_type=op_type;
303293
else
304294
{
305-
error().source_location=expr.find_source_location();
306-
error() << "no constant one of type " << op_type.pretty() << eom;
307-
throw 0;
295+
UNREACHABLE;
308296
}
309297

310298
exprt constant;
@@ -349,9 +337,13 @@ void goto_convertt::remove_function_call(
349337
const irep_idt &mode,
350338
bool result_is_used)
351339
{
340+
INVARIANT_WITH_DIAGNOSTICS(
341+
expr.operands().size() == 2,
342+
"function_call expects two operands",
343+
expr.find_source_location());
344+
352345
if(!result_is_used)
353346
{
354-
assert(expr.operands().size()==2);
355347
code_function_callt call(nil_exprt(), expr.op0(), expr.op1().operands());
356348
call.add_source_location()=expr.source_location();
357349
convert_function_call(call, dest, mode);
@@ -361,20 +353,10 @@ void goto_convertt::remove_function_call(
361353

362354
// get name of function, if available
363355

364-
if(expr.id()!=ID_side_effect ||
365-
expr.get(ID_statement)!=ID_function_call)
366-
{
367-
error().source_location=expr.find_source_location();
368-
error() << "expected function call" << eom;
369-
throw 0;
370-
}
371-
372-
if(expr.operands().empty())
373-
{
374-
error().source_location=expr.find_source_location();
375-
error() << "function_call expects at least one operand" << eom;
376-
throw 0;
377-
}
356+
INVARIANT_WITH_DIAGNOSTICS(
357+
expr.id() == ID_side_effect && expr.get(ID_statement) == ID_function_call,
358+
"expects function call",
359+
expr.find_source_location());
378360

379361
std::string new_base_name = "return_value";
380362
irep_idt new_symbol_mode = mode;
@@ -456,7 +438,7 @@ void goto_convertt::remove_cpp_delete(
456438
side_effect_exprt &expr,
457439
goto_programt &dest)
458440
{
459-
assert(expr.operands().size()==1);
441+
DATA_INVARIANT(expr.operands().size() == 1, "cpp_delete expects one operand");
460442

461443
codet tmp(expr.get_statement());
462444
tmp.add_source_location()=expr.source_location();
@@ -509,13 +491,10 @@ void goto_convertt::remove_temporary_object(
509491
goto_programt &dest)
510492
{
511493
const irep_idt &mode = expr.get(ID_mode);
512-
if(expr.operands().size()!=1 &&
513-
!expr.operands().empty())
514-
{
515-
error().source_location=expr.find_source_location();
516-
error() << "temporary_object takes 0 or 1 operands" << eom;
517-
throw 0;
518-
}
494+
INVARIANT_WITH_DIAGNOSTICS(
495+
expr.operands().size() <= 1,
496+
"temporary_object takes zero or one operands",
497+
expr.find_source_location());
519498

520499
symbolt &new_symbol = new_tmp_symbol(
521500
expr.type(), "obj", dest, expr.find_source_location(), mode);
@@ -529,7 +508,10 @@ void goto_convertt::remove_temporary_object(
529508

530509
if(expr.find(ID_initializer).is_not_nil())
531510
{
532-
assert(expr.operands().empty());
511+
INVARIANT_WITH_DIAGNOSTICS(
512+
expr.operands().empty(),
513+
"temporary_object takes zero operands",
514+
expr.find_source_location());
533515
exprt initializer=static_cast<const exprt &>(expr.find(ID_initializer));
534516
replace_new_object(new_symbol.symbol_expr(), initializer);
535517

@@ -550,19 +532,15 @@ void goto_convertt::remove_statement_expression(
550532
// The expression is copied into a temporary before the
551533
// scope is destroyed.
552534

553-
if(expr.operands().size()!=1)
554-
{
555-
error().source_location=expr.find_source_location();
556-
error() << "statement_expression takes 1 operand" << eom;
557-
throw 0;
558-
}
535+
INVARIANT_WITH_DIAGNOSTICS(
536+
expr.operands().size() == 1,
537+
"statement_expression takes one operand",
538+
expr.find_source_location());
559539

560-
if(expr.op0().id()!=ID_code)
561-
{
562-
error().source_location=expr.op0().find_source_location();
563-
error() << "statement_expression takes code as operand" << eom;
564-
throw 0;
565-
}
540+
INVARIANT_WITH_DIAGNOSTICS(
541+
expr.op0().id() == ID_code,
542+
"statement_expression takes code as operand",
543+
expr.find_source_location());
566544

567545
codet &code=to_code(expr.op0());
568546

@@ -573,20 +551,15 @@ void goto_convertt::remove_statement_expression(
573551
return;
574552
}
575553

576-
if(code.get_statement()!=ID_block)
577-
{
578-
error().source_location=code.find_source_location();
579-
error() << "statement_expression takes block as operand" << eom;
580-
throw 0;
581-
}
554+
INVARIANT_WITH_DIAGNOSTICS(
555+
code.get_statement() == ID_block,
556+
"statement_expression takes block as operand",
557+
code.find_source_location());
582558

583-
if(code.operands().empty())
584-
{
585-
error().source_location=expr.find_source_location();
586-
error() << "statement_expression takes non-empty block as operand"
587-
<< eom;
588-
throw 0;
589-
}
559+
INVARIANT_WITH_DIAGNOSTICS(
560+
!code.operands().empty(),
561+
"statement_expression takes non-empty block as operand",
562+
expr.find_source_location());
590563

591564
// get last statement from block, following labels
592565
codet &last=to_code_block(code).find_last_statement();
@@ -615,10 +588,7 @@ void goto_convertt::remove_statement_expression(
615588
}
616589
else
617590
{
618-
error() << "statement_expression expects expression as "
619-
<< "last statement, but got `"
620-
<< last.get(ID_statement) << "'" << eom;
621-
throw 0;
591+
UNREACHABLE;
622592
}
623593

624594
{
@@ -694,8 +664,6 @@ void goto_convertt::remove_side_effect(
694664
}
695665
else
696666
{
697-
error().source_location=expr.find_source_location();
698-
error() << "cannot remove side effect (" << statement << ")" << eom;
699-
throw 0;
667+
UNREACHABLE;
700668
}
701669
}

0 commit comments

Comments
 (0)