fix for calls to validate_expr

Daniel Kroening · Daniel Kroening · commit 6879ae4ae06a · 2019-04-24T11:07:36.000+01:00
diff --git a/src/util/std_code.h b/src/util/std_code.h
@@ -767,15 +767,15 @@ inline const code_ifthenelset &to_code_ifthenelse(const codet &code)
 {
   PRECONDITION(code.get_statement() == ID_ifthenelse);
   const code_ifthenelset &ret = static_cast<const code_ifthenelset &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
 inline code_ifthenelset &to_code_ifthenelse(codet &code)
 {
   PRECONDITION(code.get_statement() == ID_ifthenelse);
   code_ifthenelset &ret = static_cast<code_ifthenelset &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
@@ -829,15 +829,15 @@ inline const code_switcht &to_code_switch(const codet &code)
 {
   PRECONDITION(code.get_statement() == ID_switch);
   const code_switcht &ret = static_cast<const code_switcht &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
 inline code_switcht &to_code_switch(codet &code)
 {
   PRECONDITION(code.get_statement() == ID_switch);
   code_switcht &ret = static_cast<code_switcht &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
@@ -891,15 +891,15 @@ inline const code_whilet &to_code_while(const codet &code)
 {
   PRECONDITION(code.get_statement() == ID_while);
   const code_whilet &ret = static_cast<const code_whilet &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
 inline code_whilet &to_code_while(codet &code)
 {
   PRECONDITION(code.get_statement() == ID_while);
   code_whilet &ret = static_cast<code_whilet &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
@@ -953,15 +953,15 @@ inline const code_dowhilet &to_code_dowhile(const codet &code)
 {
   PRECONDITION(code.get_statement() == ID_dowhile);
   const code_dowhilet &ret = static_cast<const code_dowhilet &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
 inline code_dowhilet &to_code_dowhile(codet &code)
 {
   PRECONDITION(code.get_statement() == ID_dowhile);
   code_dowhilet &ret = static_cast<code_dowhilet &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
@@ -1050,15 +1050,15 @@ inline const code_fort &to_code_for(const codet &code)
 {
   PRECONDITION(code.get_statement() == ID_for);
   const code_fort &ret = static_cast<const code_fort &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
 inline code_fort &to_code_for(codet &code)
 {
   PRECONDITION(code.get_statement() == ID_for);
   code_fort &ret = static_cast<code_fort &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
@@ -1102,15 +1102,15 @@ inline const code_gotot &to_code_goto(const codet &code)
 {
   PRECONDITION(code.get_statement() == ID_goto);
   const code_gotot &ret = static_cast<const code_gotot &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
 inline code_gotot &to_code_goto(codet &code)
 {
   PRECONDITION(code.get_statement() == ID_goto);
   code_gotot &ret = static_cast<code_gotot &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
@@ -1368,15 +1368,15 @@ inline const code_labelt &to_code_label(const codet &code)
 {
   PRECONDITION(code.get_statement() == ID_label);
   const code_labelt &ret = static_cast<const code_labelt &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
 inline code_labelt &to_code_label(codet &code)
 {
   PRECONDITION(code.get_statement() == ID_label);
   code_labelt &ret = static_cast<code_labelt &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
@@ -1441,15 +1441,15 @@ inline const code_switch_caset &to_code_switch_case(const codet &code)
 {
   PRECONDITION(code.get_statement() == ID_switch_case);
   const code_switch_caset &ret = static_cast<const code_switch_caset &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
 inline code_switch_caset &to_code_switch_case(codet &code)
 {
   PRECONDITION(code.get_statement() == ID_switch_case);
   code_switch_caset &ret = static_cast<code_switch_caset &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
@@ -1526,7 +1526,7 @@ to_code_gcc_switch_case_range(const codet &code)
   PRECONDITION(code.get_statement() == ID_gcc_switch_case_range);
   const code_gcc_switch_case_ranget &ret =
     static_cast<const code_gcc_switch_case_ranget &>(code);
-  validate_expr(code);
+  //validate_expr(ret);
   return ret;
 }
 
@@ -1535,7 +1535,7 @@ inline code_gcc_switch_case_ranget &to_code_gcc_switch_case_range(codet &code)
   PRECONDITION(code.get_statement() == ID_gcc_switch_case_range);
   code_gcc_switch_case_ranget &ret =
     static_cast<code_gcc_switch_case_ranget &>(code);
-  validate_expr(code);
+  //validate_expr(ret);
   return ret;
 }
 
@@ -1722,12 +1722,6 @@ class code_asm_gcct : public code_asmt
   using code_asmt::op3;
 };
 
-template <>
-inline bool can_cast_expr<code_asm_gcct>(const exprt &base)
-{
-  return detail::can_cast_code_impl(base, ID_asm);
-}
-
 inline void validate_expr(const code_asm_gcct &x)
 {
   validate_operands(x, 5, "code_asm_gcc must have five operands");
@@ -1738,7 +1732,7 @@ inline code_asm_gcct &to_code_asm_gcc(codet &code)
   PRECONDITION(code.get_statement() == ID_asm);
   PRECONDITION(to_code_asm(code).get_flavor() == ID_gcc);
   code_asm_gcct &ret = static_cast<code_asm_gcct &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
@@ -1747,7 +1741,7 @@ inline const code_asm_gcct &to_code_asm_gcc(const codet &code)
   PRECONDITION(code.get_statement() == ID_asm);
   PRECONDITION(to_code_asm(code).get_flavor() == ID_gcc);
   const code_asm_gcct &ret = static_cast<const code_asm_gcct &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
@@ -1792,15 +1786,15 @@ inline code_expressiont &to_code_expression(codet &code)
 {
   PRECONDITION(code.get_statement() == ID_expression);
   code_expressiont &ret = static_cast<code_expressiont &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
 inline const code_expressiont &to_code_expression(const codet &code)
 {
   PRECONDITION(code.get_statement() == ID_expression);
   const code_expressiont &ret = static_cast<const code_expressiont &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
@@ -2401,15 +2395,15 @@ inline const code_try_catcht &to_code_try_catch(const codet &code)
 {
   PRECONDITION(code.get_statement() == ID_try_catch);
   const code_try_catcht &ret = static_cast<const code_try_catcht &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 
 inline code_try_catcht &to_code_try_catch(codet &code)
 {
   PRECONDITION(code.get_statement() == ID_try_catch);
   code_try_catcht &ret = static_cast<code_try_catcht &>(code);
-  validate_expr(code);
+  validate_expr(ret);
   return ret;
 }
 

Original file line number	Diff line number	Diff line change
`@@ -767,15 +767,15 @@ inline const code_ifthenelset &to_code_ifthenelse(const codet &code)`
`767`	`767`	`{`
`768`	`768`	`PRECONDITION(code.get_statement() == ID_ifthenelse);`
`769`	`769`	`const code_ifthenelset &ret = static_cast<const code_ifthenelset &>(code);`
`770`		`- validate_expr(code);`
	`770`	`+ validate_expr(ret);`
`771`	`771`	`return ret;`
`772`	`772`	`}`
`773`	`773`
`774`	`774`	`inline code_ifthenelset &to_code_ifthenelse(codet &code)`
`775`	`775`	`{`
`776`	`776`	`PRECONDITION(code.get_statement() == ID_ifthenelse);`
`777`	`777`	`code_ifthenelset &ret = static_cast<code_ifthenelset &>(code);`
`778`		`- validate_expr(code);`
	`778`	`+ validate_expr(ret);`
`779`	`779`	`return ret;`
`780`	`780`	`}`
`781`	`781`
`@@ -829,15 +829,15 @@ inline const code_switcht &to_code_switch(const codet &code)`
`829`	`829`	`{`
`830`	`830`	`PRECONDITION(code.get_statement() == ID_switch);`
`831`	`831`	`const code_switcht &ret = static_cast<const code_switcht &>(code);`
`832`		`- validate_expr(code);`
	`832`	`+ validate_expr(ret);`
`833`	`833`	`return ret;`
`834`	`834`	`}`
`835`	`835`
`836`	`836`	`inline code_switcht &to_code_switch(codet &code)`
`837`	`837`	`{`
`838`	`838`	`PRECONDITION(code.get_statement() == ID_switch);`
`839`	`839`	`code_switcht &ret = static_cast<code_switcht &>(code);`
`840`		`- validate_expr(code);`
	`840`	`+ validate_expr(ret);`
`841`	`841`	`return ret;`
`842`	`842`	`}`
`843`	`843`
`@@ -891,15 +891,15 @@ inline const code_whilet &to_code_while(const codet &code)`
`891`	`891`	`{`
`892`	`892`	`PRECONDITION(code.get_statement() == ID_while);`
`893`	`893`	`const code_whilet &ret = static_cast<const code_whilet &>(code);`
`894`		`- validate_expr(code);`
	`894`	`+ validate_expr(ret);`
`895`	`895`	`return ret;`
`896`	`896`	`}`
`897`	`897`
`898`	`898`	`inline code_whilet &to_code_while(codet &code)`
`899`	`899`	`{`
`900`	`900`	`PRECONDITION(code.get_statement() == ID_while);`
`901`	`901`	`code_whilet &ret = static_cast<code_whilet &>(code);`
`902`		`- validate_expr(code);`
	`902`	`+ validate_expr(ret);`
`903`	`903`	`return ret;`
`904`	`904`	`}`
`905`	`905`
`@@ -953,15 +953,15 @@ inline const code_dowhilet &to_code_dowhile(const codet &code)`
`953`	`953`	`{`
`954`	`954`	`PRECONDITION(code.get_statement() == ID_dowhile);`
`955`	`955`	`const code_dowhilet &ret = static_cast<const code_dowhilet &>(code);`
`956`		`- validate_expr(code);`
	`956`	`+ validate_expr(ret);`
`957`	`957`	`return ret;`
`958`	`958`	`}`
`959`	`959`
`960`	`960`	`inline code_dowhilet &to_code_dowhile(codet &code)`
`961`	`961`	`{`
`962`	`962`	`PRECONDITION(code.get_statement() == ID_dowhile);`
`963`	`963`	`code_dowhilet &ret = static_cast<code_dowhilet &>(code);`
`964`		`- validate_expr(code);`
	`964`	`+ validate_expr(ret);`
`965`	`965`	`return ret;`
`966`	`966`	`}`
`967`	`967`
`@@ -1050,15 +1050,15 @@ inline const code_fort &to_code_for(const codet &code)`
`1050`	`1050`	`{`
`1051`	`1051`	`PRECONDITION(code.get_statement() == ID_for);`
`1052`	`1052`	`const code_fort &ret = static_cast<const code_fort &>(code);`
`1053`		`- validate_expr(code);`
	`1053`	`+ validate_expr(ret);`
`1054`	`1054`	`return ret;`
`1055`	`1055`	`}`
`1056`	`1056`
`1057`	`1057`	`inline code_fort &to_code_for(codet &code)`
`1058`	`1058`	`{`
`1059`	`1059`	`PRECONDITION(code.get_statement() == ID_for);`
`1060`	`1060`	`code_fort &ret = static_cast<code_fort &>(code);`
`1061`		`- validate_expr(code);`
	`1061`	`+ validate_expr(ret);`
`1062`	`1062`	`return ret;`
`1063`	`1063`	`}`
`1064`	`1064`
`@@ -1102,15 +1102,15 @@ inline const code_gotot &to_code_goto(const codet &code)`
`1102`	`1102`	`{`
`1103`	`1103`	`PRECONDITION(code.get_statement() == ID_goto);`
`1104`	`1104`	`const code_gotot &ret = static_cast<const code_gotot &>(code);`
`1105`		`- validate_expr(code);`
	`1105`	`+ validate_expr(ret);`
`1106`	`1106`	`return ret;`
`1107`	`1107`	`}`
`1108`	`1108`
`1109`	`1109`	`inline code_gotot &to_code_goto(codet &code)`
`1110`	`1110`	`{`
`1111`	`1111`	`PRECONDITION(code.get_statement() == ID_goto);`
`1112`	`1112`	`code_gotot &ret = static_cast<code_gotot &>(code);`
`1113`		`- validate_expr(code);`
	`1113`	`+ validate_expr(ret);`
`1114`	`1114`	`return ret;`
`1115`	`1115`	`}`
`1116`	`1116`
`@@ -1368,15 +1368,15 @@ inline const code_labelt &to_code_label(const codet &code)`
`1368`	`1368`	`{`
`1369`	`1369`	`PRECONDITION(code.get_statement() == ID_label);`
`1370`	`1370`	`const code_labelt &ret = static_cast<const code_labelt &>(code);`
`1371`		`- validate_expr(code);`
	`1371`	`+ validate_expr(ret);`
`1372`	`1372`	`return ret;`
`1373`	`1373`	`}`
`1374`	`1374`
`1375`	`1375`	`inline code_labelt &to_code_label(codet &code)`
`1376`	`1376`	`{`
`1377`	`1377`	`PRECONDITION(code.get_statement() == ID_label);`
`1378`	`1378`	`code_labelt &ret = static_cast<code_labelt &>(code);`
`1379`		`- validate_expr(code);`
	`1379`	`+ validate_expr(ret);`
`1380`	`1380`	`return ret;`
`1381`	`1381`	`}`
`1382`	`1382`
`@@ -1441,15 +1441,15 @@ inline const code_switch_caset &to_code_switch_case(const codet &code)`
`1441`	`1441`	`{`
`1442`	`1442`	`PRECONDITION(code.get_statement() == ID_switch_case);`
`1443`	`1443`	`const code_switch_caset &ret = static_cast<const code_switch_caset &>(code);`
`1444`		`- validate_expr(code);`
	`1444`	`+ validate_expr(ret);`
`1445`	`1445`	`return ret;`
`1446`	`1446`	`}`
`1447`	`1447`
`1448`	`1448`	`inline code_switch_caset &to_code_switch_case(codet &code)`
`1449`	`1449`	`{`
`1450`	`1450`	`PRECONDITION(code.get_statement() == ID_switch_case);`
`1451`	`1451`	`code_switch_caset &ret = static_cast<code_switch_caset &>(code);`
`1452`		`- validate_expr(code);`
	`1452`	`+ validate_expr(ret);`
`1453`	`1453`	`return ret;`
`1454`	`1454`	`}`
`1455`	`1455`
`@@ -1526,7 +1526,7 @@ to_code_gcc_switch_case_range(const codet &code)`
`1526`	`1526`	`PRECONDITION(code.get_statement() == ID_gcc_switch_case_range);`
`1527`	`1527`	`const code_gcc_switch_case_ranget &ret =`
`1528`	`1528`	`static_cast<const code_gcc_switch_case_ranget &>(code);`
`1529`		`- validate_expr(code);`
	`1529`	`+ //validate_expr(ret);`
`1530`	`1530`	`return ret;`
`1531`	`1531`	`}`
`1532`	`1532`
`@@ -1535,7 +1535,7 @@ inline code_gcc_switch_case_ranget &to_code_gcc_switch_case_range(codet &code)`
`1535`	`1535`	`PRECONDITION(code.get_statement() == ID_gcc_switch_case_range);`
`1536`	`1536`	`code_gcc_switch_case_ranget &ret =`
`1537`	`1537`	`static_cast<code_gcc_switch_case_ranget &>(code);`
`1538`		`- validate_expr(code);`
	`1538`	`+ //validate_expr(ret);`
`1539`	`1539`	`return ret;`
`1540`	`1540`	`}`
`1541`	`1541`
`@@ -1722,12 +1722,6 @@ class code_asm_gcct : public code_asmt`
`1722`	`1722`	`using code_asmt::op3;`
`1723`	`1723`	`};`
`1724`	`1724`
`1725`		`-template <>`
`1726`		`-inline bool can_cast_expr<code_asm_gcct>(const exprt &base)`
`1727`		`-{`
`1728`		`- return detail::can_cast_code_impl(base, ID_asm);`
`1729`		`-}`
`1730`		`-`
`1731`	`1725`	`inline void validate_expr(const code_asm_gcct &x)`
`1732`	`1726`	`{`
`1733`	`1727`	`validate_operands(x, 5, "code_asm_gcc must have five operands");`
`@@ -1738,7 +1732,7 @@ inline code_asm_gcct &to_code_asm_gcc(codet &code)`
`1738`	`1732`	`PRECONDITION(code.get_statement() == ID_asm);`
`1739`	`1733`	`PRECONDITION(to_code_asm(code).get_flavor() == ID_gcc);`
`1740`	`1734`	`code_asm_gcct &ret = static_cast<code_asm_gcct &>(code);`
`1741`		`- validate_expr(code);`
	`1735`	`+ validate_expr(ret);`
`1742`	`1736`	`return ret;`
`1743`	`1737`	`}`
`1744`	`1738`
`@@ -1747,7 +1741,7 @@ inline const code_asm_gcct &to_code_asm_gcc(const codet &code)`
`1747`	`1741`	`PRECONDITION(code.get_statement() == ID_asm);`
`1748`	`1742`	`PRECONDITION(to_code_asm(code).get_flavor() == ID_gcc);`
`1749`	`1743`	`const code_asm_gcct &ret = static_cast<const code_asm_gcct &>(code);`
`1750`		`- validate_expr(code);`
	`1744`	`+ validate_expr(ret);`
`1751`	`1745`	`return ret;`
`1752`	`1746`	`}`
`1753`	`1747`
`@@ -1792,15 +1786,15 @@ inline code_expressiont &to_code_expression(codet &code)`
`1792`	`1786`	`{`
`1793`	`1787`	`PRECONDITION(code.get_statement() == ID_expression);`
`1794`	`1788`	`code_expressiont &ret = static_cast<code_expressiont &>(code);`
`1795`		`- validate_expr(code);`
	`1789`	`+ validate_expr(ret);`
`1796`	`1790`	`return ret;`
`1797`	`1791`	`}`
`1798`	`1792`
`1799`	`1793`	`inline const code_expressiont &to_code_expression(const codet &code)`
`1800`	`1794`	`{`
`1801`	`1795`	`PRECONDITION(code.get_statement() == ID_expression);`
`1802`	`1796`	`const code_expressiont &ret = static_cast<const code_expressiont &>(code);`
`1803`		`- validate_expr(code);`
	`1797`	`+ validate_expr(ret);`
`1804`	`1798`	`return ret;`
`1805`	`1799`	`}`
`1806`	`1800`
`@@ -2401,15 +2395,15 @@ inline const code_try_catcht &to_code_try_catch(const codet &code)`
`2401`	`2395`	`{`
`2402`	`2396`	`PRECONDITION(code.get_statement() == ID_try_catch);`
`2403`	`2397`	`const code_try_catcht &ret = static_cast<const code_try_catcht &>(code);`
`2404`		`- validate_expr(code);`
	`2398`	`+ validate_expr(ret);`
`2405`	`2399`	`return ret;`
`2406`	`2400`	`}`
`2407`	`2401`
`2408`	`2402`	`inline code_try_catcht &to_code_try_catch(codet &code)`
`2409`	`2403`	`{`
`2410`	`2404`	`PRECONDITION(code.get_statement() == ID_try_catch);`
`2411`	`2405`	`code_try_catcht &ret = static_cast<code_try_catcht &>(code);`
`2412`		`- validate_expr(code);`
	`2406`	`+ validate_expr(ret);`
`2413`	`2407`	`return ret;`
`2414`	`2408`	`}`
`2415`	`2409`