Merge pull request #6809 from tautschnig/bugfixes/rename-return

kroening · web-flow · commit b22ded7df5a7 · 2022-05-06T14:06:29.000-07:00
rename_symbolt: renaming in return values should affect the result
diff --git a/src/util/rename_symbol.cpp b/src/util/rename_symbol.cpp
@@ -146,7 +146,8 @@ bool rename_symbolt::rename(typet &dest) const
   else if(dest.id()==ID_code)
   {
     code_typet &code_type=to_code_type(dest);
-    rename(code_type.return_type());
+    if(!rename(code_type.return_type()))
+      result = false;
 
     for(auto &p : code_type.parameters())
     {

Original file line number	Diff line number	Diff line change
`@@ -146,7 +146,8 @@ bool rename_symbolt::rename(typet &dest) const`
`146`	`146`	`else if(dest.id()==ID_code)`
`147`	`147`	`{`
`148`	`148`	`code_typet &code_type=to_code_type(dest);`
`149`		`- rename(code_type.return_type());`
	`149`	`+ if(!rename(code_type.return_type()))`
	`150`	`+ result = false;`
`150`	`151`
`151`	`152`	`for(auto &p : code_type.parameters())`
`152`	`153`	`{`