Consistently resize instead of just reserving in codet classes

tautschnig · tautschnig · commit e527f646b5a7 · 2017-01-20T07:09:09.000-08:00
diff --git a/src/util/std_code.h b/src/util/std_code.h
@@ -281,8 +281,7 @@ class code_assumet:public codet
 public:
   inline code_assumet():codet(ID_assume)
   {
-    // will change to resize(1) in the future
-    reserve_operands(1);
+    operands().resize(1);
   }
 
   inline explicit code_assumet(const exprt &expr):codet(ID_assume)
@@ -320,8 +319,7 @@ class code_assertt:public codet
 public:
   inline code_assertt():codet(ID_assert)
   {
-    // will change to resize(1) in the future
-    reserve_operands(1);
+    operands().resize(1);
   }
 
   inline explicit code_assertt(const exprt &expr):codet(ID_assert)
@@ -723,7 +721,8 @@ class code_returnt:public codet
 public:
   inline code_returnt():codet(ID_return)
   {
-    reserve_operands(1);
+    operands().resize(1);
+    op0().make_nil();
   }
 
   explicit inline code_returnt(const exprt &_op):codet(ID_return)
@@ -738,13 +737,14 @@ class code_returnt:public codet
 
   inline exprt &return_value()
   {
-    operands().resize(1);
     return op0();
   }
 
   inline bool has_return_value() const
   {
-    return operands().size()==1;
+    if(operands().empty())
+      return false; // backwards compatibility
+    return return_value().is_not_nil();
   }
 };
 

Original file line number	Diff line number	Diff line change
`@@ -281,8 +281,7 @@ class code_assumet:public codet`
`281`	`281`	`public:`
`282`	`282`	`inline code_assumet():codet(ID_assume)`
`283`	`283`	`{`
`284`		`- // will change to resize(1) in the future`
`285`		`- reserve_operands(1);`
	`284`	`+ operands().resize(1);`
`286`	`285`	`}`
`287`	`286`
`288`	`287`	`inline explicit code_assumet(const exprt &expr):codet(ID_assume)`
`@@ -320,8 +319,7 @@ class code_assertt:public codet`
`320`	`319`	`public:`
`321`	`320`	`inline code_assertt():codet(ID_assert)`
`322`	`321`	`{`
`323`		`- // will change to resize(1) in the future`
`324`		`- reserve_operands(1);`
	`322`	`+ operands().resize(1);`
`325`	`323`	`}`
`326`	`324`
`327`	`325`	`inline explicit code_assertt(const exprt &expr):codet(ID_assert)`
`@@ -723,7 +721,8 @@ class code_returnt:public codet`
`723`	`721`	`public:`
`724`	`722`	`inline code_returnt():codet(ID_return)`
`725`	`723`	`{`
`726`		`- reserve_operands(1);`
	`724`	`+ operands().resize(1);`
	`725`	`+ op0().make_nil();`
`727`	`726`	`}`
`728`	`727`
`729`	`728`	`explicit inline code_returnt(const exprt &_op):codet(ID_return)`
`@@ -738,13 +737,14 @@ class code_returnt:public codet`
`738`	`737`
`739`	`738`	`inline exprt &return_value()`
`740`	`739`	`{`
`741`		`- operands().resize(1);`
`742`	`740`	`return op0();`
`743`	`741`	`}`
`744`	`742`
`745`	`743`	`inline bool has_return_value() const`
`746`	`744`	`{`
`747`		`- return operands().size()==1;`
	`745`	`+ if(operands().empty())`
	`746`	`+ return false; // backwards compatibility`
	`747`	`+ return return_value().is_not_nil();`
`748`	`748`	`}`
`749`	`749`	`};`
`750`	`750`