Skip to content

Commit ea1bc3a

Browse files
tautschnigtautschnig
committed
Re-use validate_expr in to_code_*t
This provides two advantages: 1) Member access such as testing the number of operands does not break sharing, because it is done in a const context. 2) Code re-use: we no longer implement the same check in two different ways. All changes in this commit were applied automatically via text replacement.
1 parent 73ea08b commit ea1bc3a

File tree

1 file changed

+86
-68
lines changed

1 file changed

+86
-68
lines changed

‎src/util/std_code.h

Lines changed: 86 additions & 68 deletions
Original file line numberDiff line numberDiff line change
@@ -549,13 +549,17 @@ inline void validate_expr(const code_assumet &x)
549549
inline const code_assumet &to_code_assume(const codet &code)
550550
{
551551
PRECONDITION(code.get_statement() == ID_assume);
552-
return static_cast<const code_assumet &>(code);
552+
const code_assumet &ret = static_cast<const code_assumet &>(code);
553+
validate_expr(ret);
554+
return ret;
553555
}
554556

555557
inline code_assumet &to_code_assume(codet &code)
556558
{
557559
PRECONDITION(code.get_statement() == ID_assume);
558-
return static_cast<code_assumet &>(code);
560+
code_assumet &ret = static_cast<code_assumet &>(code);
561+
validate_expr(ret);
562+
return ret;
559563
}
560564

561565
/// A non-fatal assertion, which checks a condition then permits execution to
@@ -603,13 +607,17 @@ inline void validate_expr(const code_assertt &x)
603607
inline const code_assertt &to_code_assert(const codet &code)
604608
{
605609
PRECONDITION(code.get_statement() == ID_assert);
606-
return static_cast<const code_assertt &>(code);
610+
const code_assertt &ret = static_cast<const code_assertt &>(code);
611+
validate_expr(ret);
612+
return ret;
607613
}
608614

609615
inline code_assertt &to_code_assert(codet &code)
610616
{
611617
PRECONDITION(code.get_statement() == ID_assert);
612-
return static_cast<code_assertt &>(code);
618+
code_assertt &ret = static_cast<code_assertt &>(code);
619+
validate_expr(ret);
620+
return ret;
613621
}
614622

615623
/// Create a fatal assertion, which checks a condition and then halts if it does
@@ -709,17 +717,17 @@ inline void validate_expr(const code_ifthenelset &x)
709717
inline const code_ifthenelset &to_code_ifthenelse(const codet &code)
710718
{
711719
PRECONDITION(code.get_statement() == ID_ifthenelse);
712-
DATA_INVARIANT(
713-
code.operands().size() == 3, "if-then-else must have three operands");
714-
return static_cast<const code_ifthenelset &>(code);
720+
const code_ifthenelset &ret = static_cast<const code_ifthenelset &>(code);
721+
validate_expr(code);
722+
return ret;
715723
}
716724

717725
inline code_ifthenelset &to_code_ifthenelse(codet &code)
718726
{
719727
PRECONDITION(code.get_statement() == ID_ifthenelse);
720-
DATA_INVARIANT(
721-
code.operands().size() == 3, "if-then-else must have three operands");
722-
return static_cast<code_ifthenelset &>(code);
728+
code_ifthenelset &ret = static_cast<code_ifthenelset &>(code);
729+
validate_expr(code);
730+
return ret;
723731
}
724732

725733
/// \ref codet representing a `switch` statement.
@@ -777,15 +785,17 @@ inline void validate_expr(const code_switcht &x)
777785
inline const code_switcht &to_code_switch(const codet &code)
778786
{
779787
PRECONDITION(code.get_statement() == ID_switch);
780-
DATA_INVARIANT(code.operands().size() == 2, "switch must have two operands");
781-
return static_cast<const code_switcht &>(code);
788+
const code_switcht &ret = static_cast<const code_switcht &>(code);
789+
validate_expr(code);
790+
return ret;
782791
}
783792

784793
inline code_switcht &to_code_switch(codet &code)
785794
{
786795
PRECONDITION(code.get_statement() == ID_switch);
787-
DATA_INVARIANT(code.operands().size() == 2, "switch must have two operands");
788-
return static_cast<code_switcht &>(code);
796+
code_switcht &ret = static_cast<code_switcht &>(code);
797+
validate_expr(code);
798+
return ret;
789799
}
790800

791801
/// \ref codet representing a `while` statement.
@@ -843,15 +853,17 @@ inline void validate_expr(const code_whilet &x)
843853
inline const code_whilet &to_code_while(const codet &code)
844854
{
845855
PRECONDITION(code.get_statement() == ID_while);
846-
DATA_INVARIANT(code.operands().size() == 2, "while must have two operands");
847-
return static_cast<const code_whilet &>(code);
856+
const code_whilet &ret = static_cast<const code_whilet &>(code);
857+
validate_expr(code);
858+
return ret;
848859
}
849860

850861
inline code_whilet &to_code_while(codet &code)
851862
{
852863
PRECONDITION(code.get_statement() == ID_while);
853-
DATA_INVARIANT(code.operands().size() == 2, "while must have two operands");
854-
return static_cast<code_whilet &>(code);
864+
code_whilet &ret = static_cast<code_whilet &>(code);
865+
validate_expr(code);
866+
return ret;
855867
}
856868

857869
/// \ref codet representation of a `do while` statement.
@@ -909,17 +921,17 @@ inline void validate_expr(const code_dowhilet &x)
909921
inline const code_dowhilet &to_code_dowhile(const codet &code)
910922
{
911923
PRECONDITION(code.get_statement() == ID_dowhile);
912-
DATA_INVARIANT(
913-
code.operands().size() == 2, "do-while must have two operands");
914-
return static_cast<const code_dowhilet &>(code);
924+
const code_dowhilet &ret = static_cast<const code_dowhilet &>(code);
925+
validate_expr(code);
926+
return ret;
915927
}
916928

917929
inline code_dowhilet &to_code_dowhile(codet &code)
918930
{
919931
PRECONDITION(code.get_statement() == ID_dowhile);
920-
DATA_INVARIANT(
921-
code.operands().size() == 2, "do-while must have two operands");
922-
return static_cast<code_dowhilet &>(code);
932+
code_dowhilet &ret = static_cast<code_dowhilet &>(code);
933+
validate_expr(code);
934+
return ret;
923935
}
924936

925937
/// \ref codet representation of a `for` statement.
@@ -1004,15 +1016,17 @@ inline void validate_expr(const code_fort &x)
10041016
inline const code_fort &to_code_for(const codet &code)
10051017
{
10061018
PRECONDITION(code.get_statement() == ID_for);
1007-
DATA_INVARIANT(code.operands().size() == 4, "for must have four operands");
1008-
return static_cast<const code_fort &>(code);
1019+
const code_fort &ret = static_cast<const code_fort &>(code);
1020+
validate_expr(code);
1021+
return ret;
10091022
}
10101023

10111024
inline code_fort &to_code_for(codet &code)
10121025
{
10131026
PRECONDITION(code.get_statement() == ID_for);
1014-
DATA_INVARIANT(code.operands().size() == 4, "for must have four operands");
1015-
return static_cast<code_fort &>(code);
1027+
code_fort &ret = static_cast<code_fort &>(code);
1028+
validate_expr(code);
1029+
return ret;
10161030
}
10171031

10181032
/// \ref codet representation of a `goto` statement.
@@ -1059,15 +1073,17 @@ inline void validate_expr(const code_gotot &x)
10591073
inline const code_gotot &to_code_goto(const codet &code)
10601074
{
10611075
PRECONDITION(code.get_statement() == ID_goto);
1062-
DATA_INVARIANT(code.operands().empty(), "goto must not have operands");
1063-
return static_cast<const code_gotot &>(code);
1076+
const code_gotot &ret = static_cast<const code_gotot &>(code);
1077+
validate_expr(code);
1078+
return ret;
10641079
}
10651080

10661081
inline code_gotot &to_code_goto(codet &code)
10671082
{
10681083
PRECONDITION(code.get_statement() == ID_goto);
1069-
DATA_INVARIANT(code.operands().empty(), "goto must not have operands");
1070-
return static_cast<code_gotot &>(code);
1084+
code_gotot &ret = static_cast<code_gotot &>(code);
1085+
validate_expr(code);
1086+
return ret;
10711087
}
10721088

10731089
/// \ref codet representation of a function call statement.
@@ -1357,15 +1373,17 @@ inline void validate_expr(const code_labelt &x)
13571373
inline const code_labelt &to_code_label(const codet &code)
13581374
{
13591375
PRECONDITION(code.get_statement() == ID_label);
1360-
DATA_INVARIANT(code.operands().size() == 1, "label must have one operand");
1361-
return static_cast<const code_labelt &>(code);
1376+
const code_labelt &ret = static_cast<const code_labelt &>(code);
1377+
validate_expr(code);
1378+
return ret;
13621379
}
13631380

13641381
inline code_labelt &to_code_label(codet &code)
13651382
{
13661383
PRECONDITION(code.get_statement() == ID_label);
1367-
DATA_INVARIANT(code.operands().size() == 1, "label must have one operand");
1368-
return static_cast<code_labelt &>(code);
1384+
code_labelt &ret = static_cast<code_labelt &>(code);
1385+
validate_expr(code);
1386+
return ret;
13691387
}
13701388

13711389
/// \ref codet representation of a switch-case, i.e.\ a `case` statement within
@@ -1434,17 +1452,17 @@ inline void validate_expr(const code_switch_caset &x)
14341452
inline const code_switch_caset &to_code_switch_case(const codet &code)
14351453
{
14361454
PRECONDITION(code.get_statement() == ID_switch_case);
1437-
DATA_INVARIANT(
1438-
code.operands().size() == 2, "switch-case must have two operands");
1439-
return static_cast<const code_switch_caset &>(code);
1455+
const code_switch_caset &ret = static_cast<const code_switch_caset &>(code);
1456+
validate_expr(code);
1457+
return ret;
14401458
}
14411459

14421460
inline code_switch_caset &to_code_switch_case(codet &code)
14431461
{
14441462
PRECONDITION(code.get_statement() == ID_switch_case);
1445-
DATA_INVARIANT(
1446-
code.operands().size() == 2, "switch-case must have two operands");
1447-
return static_cast<code_switch_caset &>(code);
1463+
code_switch_caset &ret = static_cast<code_switch_caset &>(code);
1464+
validate_expr(code);
1465+
return ret;
14481466
}
14491467

14501468
/// \ref codet representation of a switch-case, i.e.\ a `case` statement
@@ -1518,19 +1536,19 @@ inline const code_gcc_switch_case_ranget &
15181536
to_code_gcc_switch_case_range(const codet &code)
15191537
{
15201538
PRECONDITION(code.get_statement() == ID_gcc_switch_case_range);
1521-
DATA_INVARIANT(
1522-
code.operands().size() == 3,
1523-
"gcc-switch-case-range must have three operands");
1524-
return static_cast<const code_gcc_switch_case_ranget &>(code);
1539+
const code_gcc_switch_case_ranget &ret =
1540+
static_cast<const code_gcc_switch_case_ranget &>(code);
1541+
validate_expr(code);
1542+
return ret;
15251543
}
15261544

15271545
inline code_gcc_switch_case_ranget &to_code_gcc_switch_case_range(codet &code)
15281546
{
15291547
PRECONDITION(code.get_statement() == ID_gcc_switch_case_range);
1530-
DATA_INVARIANT(
1531-
code.operands().size() == 3,
1532-
"gcc-switch-case-range must have three operands");
1533-
return static_cast<code_gcc_switch_case_ranget &>(code);
1548+
code_gcc_switch_case_ranget &ret =
1549+
static_cast<code_gcc_switch_case_ranget &>(code);
1550+
validate_expr(code);
1551+
return ret;
15341552
}
15351553

15361554
/// \ref codet representation of a `break` statement (within a `for` or `while`
@@ -1731,18 +1749,18 @@ inline code_asm_gcct &to_code_asm_gcc(codet &code)
17311749
{
17321750
PRECONDITION(code.get_statement() == ID_asm);
17331751
PRECONDITION(to_code_asm(code).get_flavor() == ID_gcc);
1734-
DATA_INVARIANT(
1735-
code.operands().size() == 5, "code_asm_gcc must have give operands");
1736-
return static_cast<code_asm_gcct &>(code);
1752+
code_asm_gcct &ret = static_cast<code_asm_gcct &>(code);
1753+
validate_expr(code);
1754+
return ret;
17371755
}
17381756

17391757
inline const code_asm_gcct &to_code_asm_gcc(const codet &code)
17401758
{
17411759
PRECONDITION(code.get_statement() == ID_asm);
17421760
PRECONDITION(to_code_asm(code).get_flavor() == ID_gcc);
1743-
DATA_INVARIANT(
1744-
code.operands().size() == 5, "code_asm_gcc must have give operands");
1745-
return static_cast<const code_asm_gcct &>(code);
1761+
const code_asm_gcct &ret = static_cast<const code_asm_gcct &>(code);
1762+
validate_expr(code);
1763+
return ret;
17461764
}
17471765

17481766
/// \ref codet representation of an expression statement.
@@ -1790,17 +1808,17 @@ inline void validate_expr(const code_expressiont &x)
17901808
inline code_expressiont &to_code_expression(codet &code)
17911809
{
17921810
PRECONDITION(code.get_statement() == ID_expression);
1793-
DATA_INVARIANT(
1794-
code.operands().size() == 1, "expression statement must have one operand");
1795-
return static_cast<code_expressiont &>(code);
1811+
code_expressiont &ret = static_cast<code_expressiont &>(code);
1812+
validate_expr(code);
1813+
return ret;
17961814
}
17971815

17981816
inline const code_expressiont &to_code_expression(const codet &code)
17991817
{
18001818
PRECONDITION(code.get_statement() == ID_expression);
1801-
DATA_INVARIANT(
1802-
code.operands().size() == 1, "expression statement must have one operand");
1803-
return static_cast<const code_expressiont &>(code);
1819+
const code_expressiont &ret = static_cast<const code_expressiont &>(code);
1820+
validate_expr(code);
1821+
return ret;
18041822
}
18051823

18061824
/// An expression containing a side effect.
@@ -2443,17 +2461,17 @@ inline void validate_expr(const code_try_catcht &x)
24432461
inline const code_try_catcht &to_code_try_catch(const codet &code)
24442462
{
24452463
PRECONDITION(code.get_statement() == ID_try_catch);
2446-
DATA_INVARIANT(
2447-
code.operands().size() >= 3, "try-catch must have three or more operands");
2448-
return static_cast<const code_try_catcht &>(code);
2464+
const code_try_catcht &ret = static_cast<const code_try_catcht &>(code);
2465+
validate_expr(code);
2466+
return ret;
24492467
}
24502468

24512469
inline code_try_catcht &to_code_try_catch(codet &code)
24522470
{
24532471
PRECONDITION(code.get_statement() == ID_try_catch);
2454-
DATA_INVARIANT(
2455-
code.operands().size() >= 3, "try-catch must have three or more operands");
2456-
return static_cast<code_try_catcht &>(code);
2472+
code_try_catcht &ret = static_cast<code_try_catcht &>(code);
2473+
validate_expr(code);
2474+
return ret;
24572475
}
24582476

24592477
#endif // CPROVER_UTIL_STD_CODE_H

0 commit comments

Comments
 (0)