@@ -571,8 +571,10 @@ template<> inline bool can_cast_expr<code_assumet>(const exprt &base)
571
571
return detail::can_cast_code_impl (base, ID_assume);
572
572
}
573
573
574
- // to_code_assume only checks the code statement, so no validate_expr is
575
- // provided for code_assumet
574
+ inline void validate_expr (const code_assumet &x)
575
+ {
576
+ validate_operands (x, 1 , " assume must have one operand" );
577
+ }
576
578
577
579
inline const code_assumet &to_code_assume (const codet &code)
578
580
{
@@ -586,11 +588,6 @@ inline code_assumet &to_code_assume(codet &code)
586
588
return static_cast <code_assumet &>(code);
587
589
}
588
590
589
- inline void validate_expr (const code_assumet &x)
590
- {
591
- validate_operands (x, 1 , " assume must have one operand" );
592
- }
593
-
594
591
// / A non-fatal assertion, which checks a condition then permits execution to
595
592
// / continue.
596
593
class code_assertt :public codet
@@ -628,8 +625,10 @@ template<> inline bool can_cast_expr<code_assertt>(const exprt &base)
628
625
return detail::can_cast_code_impl (base, ID_assert);
629
626
}
630
627
631
- // to_code_assert only checks the code statement, so no validate_expr is
632
- // provided for code_assertt
628
+ inline void validate_expr (const code_assertt &x)
629
+ {
630
+ validate_operands (x, 1 , " assert must have one operand" );
631
+ }
633
632
634
633
inline const code_assertt &to_code_assert (const codet &code)
635
634
{
@@ -643,11 +642,6 @@ inline code_assertt &to_code_assert(codet &code)
643
642
return static_cast <code_assertt &>(code);
644
643
}
645
644
646
- inline void validate_expr (const code_assertt &x)
647
- {
648
- validate_operands (x, 1 , " assert must have one operand" );
649
- }
650
-
651
645
// / Create a fatal assertion, which checks a condition and then halts if it does
652
646
// / not hold. Equivalent to `ASSERT(condition); ASSUME(condition)`.
653
647
// /
@@ -1246,8 +1240,10 @@ template<> inline bool can_cast_expr<code_function_callt>(const exprt &base)
1246
1240
return detail::can_cast_code_impl (base, ID_function_call);
1247
1241
}
1248
1242
1249
- // to_code_function_call only checks the code statement, so no validate_expr is
1250
- // provided for code_function_callt
1243
+ inline void validate_expr (const code_function_callt &x)
1244
+ {
1245
+ validate_operands (x, 3 , " function calls must have three operands" );
1246
+ }
1251
1247
1252
1248
inline const code_function_callt &to_code_function_call (const codet &code)
1253
1249
{
@@ -1261,11 +1257,6 @@ inline code_function_callt &to_code_function_call(codet &code)
1261
1257
return static_cast <code_function_callt &>(code);
1262
1258
}
1263
1259
1264
- inline void validate_expr (const code_function_callt &x)
1265
- {
1266
- validate_operands (x, 3 , " function calls must have three operands" );
1267
- }
1268
-
1269
1260
// / \ref codet representation of a "return from a function" statement.
1270
1261
class code_returnt :public codet
1271
1262
{
@@ -1312,8 +1303,10 @@ template<> inline bool can_cast_expr<code_returnt>(const exprt &base)
1312
1303
return detail::can_cast_code_impl (base, ID_return);
1313
1304
}
1314
1305
1315
- // to_code_return only checks the code statement, so no validate_expr is
1316
- // provided for code_returnt
1306
+ inline void validate_expr (const code_returnt &x)
1307
+ {
1308
+ validate_operands (x, 1 , " return must have one operand" );
1309
+ }
1317
1310
1318
1311
inline const code_returnt &to_code_return (const codet &code)
1319
1312
{
@@ -1327,11 +1320,6 @@ inline code_returnt &to_code_return(codet &code)
1327
1320
return static_cast <code_returnt &>(code);
1328
1321
}
1329
1322
1330
- inline void validate_expr (const code_returnt &x)
1331
- {
1332
- validate_operands (x, 1 , " return must have one operand" );
1333
- }
1334
-
1335
1323
// / \ref codet representation of a label for branch targets.
1336
1324
class code_labelt :public codet
1337
1325
{
@@ -1760,8 +1748,10 @@ inline bool can_cast_expr<code_asm_gcct>(const exprt &base)
1760
1748
return detail::can_cast_code_impl (base, ID_asm);
1761
1749
}
1762
1750
1763
- // to_code_asm_gcc only checks the code statement, so no validate_expr is
1764
- // provided for code_asmt
1751
+ inline void validate_expr (const code_asm_gcct &x)
1752
+ {
1753
+ validate_operands (x, 5 , " code_asm_gcc must have five operands" );
1754
+ }
1765
1755
1766
1756
inline code_asm_gcct &to_code_asm_gcc (codet &code)
1767
1757
{
0 commit comments