@@ -562,13 +562,17 @@ inline void validate_expr(const code_assumet &x)
562
562
inline const code_assumet &to_code_assume (const codet &code)
563
563
{
564
564
PRECONDITION (code.get_statement () == ID_assume);
565
- return static_cast <const code_assumet &>(code);
565
+ const code_assumet &ret = static_cast <const code_assumet &>(code);
566
+ validate_expr (ret);
567
+ return ret;
566
568
}
567
569
568
570
inline code_assumet &to_code_assume (codet &code)
569
571
{
570
572
PRECONDITION (code.get_statement () == ID_assume);
571
- return static_cast <code_assumet &>(code);
573
+ code_assumet &ret = static_cast <code_assumet &>(code);
574
+ validate_expr (ret);
575
+ return ret;
572
576
}
573
577
574
578
// / A non-fatal assertion, which checks a condition then permits execution to
@@ -616,13 +620,17 @@ inline void validate_expr(const code_assertt &x)
616
620
inline const code_assertt &to_code_assert (const codet &code)
617
621
{
618
622
PRECONDITION (code.get_statement () == ID_assert);
619
- return static_cast <const code_assertt &>(code);
623
+ const code_assertt &ret = static_cast <const code_assertt &>(code);
624
+ validate_expr (ret);
625
+ return ret;
620
626
}
621
627
622
628
inline code_assertt &to_code_assert (codet &code)
623
629
{
624
630
PRECONDITION (code.get_statement () == ID_assert);
625
- return static_cast <code_assertt &>(code);
631
+ code_assertt &ret = static_cast <code_assertt &>(code);
632
+ validate_expr (ret);
633
+ return ret;
626
634
}
627
635
628
636
// / Create a fatal assertion, which checks a condition and then halts if it does
@@ -722,17 +730,17 @@ inline void validate_expr(const code_ifthenelset &x)
722
730
inline const code_ifthenelset &to_code_ifthenelse (const codet &code)
723
731
{
724
732
PRECONDITION (code.get_statement () == ID_ifthenelse);
725
- DATA_INVARIANT (
726
- code. operands (). size () == 3 , " if-then-else must have three operands " );
727
- return static_cast < const code_ifthenelset &>(code) ;
733
+ const code_ifthenelset &ret = static_cast < const code_ifthenelset &>(code);
734
+ validate_expr (code );
735
+ return ret ;
728
736
}
729
737
730
738
inline code_ifthenelset &to_code_ifthenelse (codet &code)
731
739
{
732
740
PRECONDITION (code.get_statement () == ID_ifthenelse);
733
- DATA_INVARIANT (
734
- code. operands (). size () == 3 , " if-then-else must have three operands " );
735
- return static_cast <code_ifthenelset &>(code) ;
741
+ code_ifthenelset &ret = static_cast <code_ifthenelset &>(code);
742
+ validate_expr (code );
743
+ return ret ;
736
744
}
737
745
738
746
// / \ref codet representing a `switch` statement.
@@ -790,15 +798,17 @@ inline void validate_expr(const code_switcht &x)
790
798
inline const code_switcht &to_code_switch (const codet &code)
791
799
{
792
800
PRECONDITION (code.get_statement () == ID_switch);
793
- DATA_INVARIANT (code.operands ().size () == 2 , " switch must have two operands" );
794
- return static_cast <const code_switcht &>(code);
801
+ const code_switcht &ret = static_cast <const code_switcht &>(code);
802
+ validate_expr (code);
803
+ return ret;
795
804
}
796
805
797
806
inline code_switcht &to_code_switch (codet &code)
798
807
{
799
808
PRECONDITION (code.get_statement () == ID_switch);
800
- DATA_INVARIANT (code.operands ().size () == 2 , " switch must have two operands" );
801
- return static_cast <code_switcht &>(code);
809
+ code_switcht &ret = static_cast <code_switcht &>(code);
810
+ validate_expr (code);
811
+ return ret;
802
812
}
803
813
804
814
// / \ref codet representing a `while` statement.
@@ -856,15 +866,17 @@ inline void validate_expr(const code_whilet &x)
856
866
inline const code_whilet &to_code_while (const codet &code)
857
867
{
858
868
PRECONDITION (code.get_statement () == ID_while);
859
- DATA_INVARIANT (code.operands ().size () == 2 , " while must have two operands" );
860
- return static_cast <const code_whilet &>(code);
869
+ const code_whilet &ret = static_cast <const code_whilet &>(code);
870
+ validate_expr (code);
871
+ return ret;
861
872
}
862
873
863
874
inline code_whilet &to_code_while (codet &code)
864
875
{
865
876
PRECONDITION (code.get_statement () == ID_while);
866
- DATA_INVARIANT (code.operands ().size () == 2 , " while must have two operands" );
867
- return static_cast <code_whilet &>(code);
877
+ code_whilet &ret = static_cast <code_whilet &>(code);
878
+ validate_expr (code);
879
+ return ret;
868
880
}
869
881
870
882
// / \ref codet representation of a `do while` statement.
@@ -922,17 +934,17 @@ inline void validate_expr(const code_dowhilet &x)
922
934
inline const code_dowhilet &to_code_dowhile (const codet &code)
923
935
{
924
936
PRECONDITION (code.get_statement () == ID_dowhile);
925
- DATA_INVARIANT (
926
- code. operands (). size () == 2 , " do-while must have two operands " );
927
- return static_cast < const code_dowhilet &>(code) ;
937
+ const code_dowhilet &ret = static_cast < const code_dowhilet &>(code);
938
+ validate_expr (code );
939
+ return ret ;
928
940
}
929
941
930
942
inline code_dowhilet &to_code_dowhile (codet &code)
931
943
{
932
944
PRECONDITION (code.get_statement () == ID_dowhile);
933
- DATA_INVARIANT (
934
- code. operands (). size () == 2 , " do-while must have two operands " );
935
- return static_cast <code_dowhilet &>(code) ;
945
+ code_dowhilet &ret = static_cast <code_dowhilet &>(code);
946
+ validate_expr (code );
947
+ return ret ;
936
948
}
937
949
938
950
// / \ref codet representation of a `for` statement.
@@ -1017,15 +1029,17 @@ inline void validate_expr(const code_fort &x)
1017
1029
inline const code_fort &to_code_for (const codet &code)
1018
1030
{
1019
1031
PRECONDITION (code.get_statement () == ID_for);
1020
- DATA_INVARIANT (code.operands ().size () == 4 , " for must have four operands" );
1021
- return static_cast <const code_fort &>(code);
1032
+ const code_fort &ret = static_cast <const code_fort &>(code);
1033
+ validate_expr (code);
1034
+ return ret;
1022
1035
}
1023
1036
1024
1037
inline code_fort &to_code_for (codet &code)
1025
1038
{
1026
1039
PRECONDITION (code.get_statement () == ID_for);
1027
- DATA_INVARIANT (code.operands ().size () == 4 , " for must have four operands" );
1028
- return static_cast <code_fort &>(code);
1040
+ code_fort &ret = static_cast <code_fort &>(code);
1041
+ validate_expr (code);
1042
+ return ret;
1029
1043
}
1030
1044
1031
1045
// / \ref codet representation of a `goto` statement.
@@ -1072,15 +1086,17 @@ inline void validate_expr(const code_gotot &x)
1072
1086
inline const code_gotot &to_code_goto (const codet &code)
1073
1087
{
1074
1088
PRECONDITION (code.get_statement () == ID_goto);
1075
- DATA_INVARIANT (code.operands ().empty (), " goto must not have operands" );
1076
- return static_cast <const code_gotot &>(code);
1089
+ const code_gotot &ret = static_cast <const code_gotot &>(code);
1090
+ validate_expr (code);
1091
+ return ret;
1077
1092
}
1078
1093
1079
1094
inline code_gotot &to_code_goto (codet &code)
1080
1095
{
1081
1096
PRECONDITION (code.get_statement () == ID_goto);
1082
- DATA_INVARIANT (code.operands ().empty (), " goto must not have operands" );
1083
- return static_cast <code_gotot &>(code);
1097
+ code_gotot &ret = static_cast <code_gotot &>(code);
1098
+ validate_expr (code);
1099
+ return ret;
1084
1100
}
1085
1101
1086
1102
// / \ref codet representation of a function call statement.
@@ -1370,15 +1386,17 @@ inline void validate_expr(const code_labelt &x)
1370
1386
inline const code_labelt &to_code_label (const codet &code)
1371
1387
{
1372
1388
PRECONDITION (code.get_statement () == ID_label);
1373
- DATA_INVARIANT (code.operands ().size () == 1 , " label must have one operand" );
1374
- return static_cast <const code_labelt &>(code);
1389
+ const code_labelt &ret = static_cast <const code_labelt &>(code);
1390
+ validate_expr (code);
1391
+ return ret;
1375
1392
}
1376
1393
1377
1394
inline code_labelt &to_code_label (codet &code)
1378
1395
{
1379
1396
PRECONDITION (code.get_statement () == ID_label);
1380
- DATA_INVARIANT (code.operands ().size () == 1 , " label must have one operand" );
1381
- return static_cast <code_labelt &>(code);
1397
+ code_labelt &ret = static_cast <code_labelt &>(code);
1398
+ validate_expr (code);
1399
+ return ret;
1382
1400
}
1383
1401
1384
1402
// / \ref codet representation of a switch-case, i.e.\ a `case` statement within
@@ -1447,17 +1465,17 @@ inline void validate_expr(const code_switch_caset &x)
1447
1465
inline const code_switch_caset &to_code_switch_case (const codet &code)
1448
1466
{
1449
1467
PRECONDITION (code.get_statement () == ID_switch_case);
1450
- DATA_INVARIANT (
1451
- code. operands (). size () == 2 , " switch-case must have two operands " );
1452
- return static_cast < const code_switch_caset &>(code) ;
1468
+ const code_switch_caset &ret = static_cast < const code_switch_caset &>(code);
1469
+ validate_expr (code );
1470
+ return ret ;
1453
1471
}
1454
1472
1455
1473
inline code_switch_caset &to_code_switch_case (codet &code)
1456
1474
{
1457
1475
PRECONDITION (code.get_statement () == ID_switch_case);
1458
- DATA_INVARIANT (
1459
- code. operands (). size () == 2 , " switch-case must have two operands " );
1460
- return static_cast <code_switch_caset &>(code) ;
1476
+ code_switch_caset &ret = static_cast <code_switch_caset &>(code);
1477
+ validate_expr (code );
1478
+ return ret ;
1461
1479
}
1462
1480
1463
1481
// / \ref codet representation of a switch-case, i.e.\ a `case` statement
@@ -1531,19 +1549,19 @@ inline const code_gcc_switch_case_ranget &
1531
1549
to_code_gcc_switch_case_range (const codet &code)
1532
1550
{
1533
1551
PRECONDITION (code.get_statement () == ID_gcc_switch_case_range);
1534
- DATA_INVARIANT (
1535
- code. operands (). size () == 3 ,
1536
- " gcc-switch-case-range must have three operands " );
1537
- return static_cast < const code_gcc_switch_case_ranget &>(code) ;
1552
+ const code_gcc_switch_case_ranget &ret =
1553
+ static_cast < const code_gcc_switch_case_ranget &>(code);
1554
+ validate_expr (code );
1555
+ return ret ;
1538
1556
}
1539
1557
1540
1558
inline code_gcc_switch_case_ranget &to_code_gcc_switch_case_range (codet &code)
1541
1559
{
1542
1560
PRECONDITION (code.get_statement () == ID_gcc_switch_case_range);
1543
- DATA_INVARIANT (
1544
- code. operands (). size () == 3 ,
1545
- " gcc-switch-case-range must have three operands " );
1546
- return static_cast <code_gcc_switch_case_ranget &>(code) ;
1561
+ code_gcc_switch_case_ranget &ret =
1562
+ static_cast <code_gcc_switch_case_ranget &>(code);
1563
+ validate_expr (code );
1564
+ return ret ;
1547
1565
}
1548
1566
1549
1567
// / \ref codet representation of a `break` statement (within a `for` or `while`
@@ -1744,18 +1762,18 @@ inline code_asm_gcct &to_code_asm_gcc(codet &code)
1744
1762
{
1745
1763
PRECONDITION (code.get_statement () == ID_asm);
1746
1764
PRECONDITION (to_code_asm (code).get_flavor () == ID_gcc);
1747
- DATA_INVARIANT (
1748
- code. operands (). size () == 5 , " code_asm_gcc must have give operands " );
1749
- return static_cast <code_asm_gcct &>(code) ;
1765
+ code_asm_gcct &ret = static_cast <code_asm_gcct &>(code);
1766
+ validate_expr (code );
1767
+ return ret ;
1750
1768
}
1751
1769
1752
1770
inline const code_asm_gcct &to_code_asm_gcc (const codet &code)
1753
1771
{
1754
1772
PRECONDITION (code.get_statement () == ID_asm);
1755
1773
PRECONDITION (to_code_asm (code).get_flavor () == ID_gcc);
1756
- DATA_INVARIANT (
1757
- code. operands (). size () == 5 , " code_asm_gcc must have give operands " );
1758
- return static_cast < const code_asm_gcct &>(code) ;
1774
+ const code_asm_gcct &ret = static_cast < const code_asm_gcct &>(code);
1775
+ validate_expr (code );
1776
+ return ret ;
1759
1777
}
1760
1778
1761
1779
// / \ref codet representation of an expression statement.
@@ -1803,17 +1821,17 @@ inline void validate_expr(const code_expressiont &x)
1803
1821
inline code_expressiont &to_code_expression (codet &code)
1804
1822
{
1805
1823
PRECONDITION (code.get_statement () == ID_expression);
1806
- DATA_INVARIANT (
1807
- code. operands (). size () == 1 , " expression statement must have one operand " );
1808
- return static_cast <code_expressiont &>(code) ;
1824
+ code_expressiont &ret = static_cast <code_expressiont &>(code);
1825
+ validate_expr (code );
1826
+ return ret ;
1809
1827
}
1810
1828
1811
1829
inline const code_expressiont &to_code_expression (const codet &code)
1812
1830
{
1813
1831
PRECONDITION (code.get_statement () == ID_expression);
1814
- DATA_INVARIANT (
1815
- code. operands (). size () == 1 , " expression statement must have one operand " );
1816
- return static_cast < const code_expressiont &>(code) ;
1832
+ const code_expressiont &ret = static_cast < const code_expressiont &>(code);
1833
+ validate_expr (code );
1834
+ return ret ;
1817
1835
}
1818
1836
1819
1837
// / An expression containing a side effect.
@@ -2456,17 +2474,17 @@ inline void validate_expr(const code_try_catcht &x)
2456
2474
inline const code_try_catcht &to_code_try_catch (const codet &code)
2457
2475
{
2458
2476
PRECONDITION (code.get_statement () == ID_try_catch);
2459
- DATA_INVARIANT (
2460
- code. operands (). size () >= 3 , " try-catch must have three or more operands " );
2461
- return static_cast < const code_try_catcht &>(code) ;
2477
+ const code_try_catcht &ret = static_cast < const code_try_catcht &>(code);
2478
+ validate_expr (code );
2479
+ return ret ;
2462
2480
}
2463
2481
2464
2482
inline code_try_catcht &to_code_try_catch (codet &code)
2465
2483
{
2466
2484
PRECONDITION (code.get_statement () == ID_try_catch);
2467
- DATA_INVARIANT (
2468
- code. operands (). size () >= 3 , " try-catch must have three or more operands " );
2469
- return static_cast <code_try_catcht &>(code) ;
2485
+ code_try_catcht &ret = static_cast <code_try_catcht &>(code);
2486
+ validate_expr (code );
2487
+ return ret ;
2470
2488
}
2471
2489
2472
2490
// / This class is used to interface between a language frontend
0 commit comments