rvalue variant of code_blockt::add

Daniel Kroening · Daniel Kroening · commit 16d69349250e · 2018-10-07T17:29:43.000+01:00
diff --git a/src/util/std_code.h b/src/util/std_code.h
@@ -138,6 +138,11 @@ class code_blockt:public codet
     copy_to_operands(code);
   }
 
+  void add(codet &&code)
+  {
+    copy_to_operands(std::move(code));
+  }
+
   void add(codet code, const source_locationt &loc)
   {
     code.add_source_location() = loc;

Original file line number	Diff line number	Diff line change
`@@ -138,6 +138,11 @@ class code_blockt:public codet`
`138`	`138`	`copy_to_operands(code);`
`139`	`139`	`}`
`140`	`140`
	`141`	`+ void add(codet &&code)`
	`142`	`+ {`
	`143`	`+ copy_to_operands(std::move(code));`
	`144`	`+ }`
	`145`	`+`
`141`	`146`	`void add(codet code, const source_locationt &loc)`
`142`	`147`	`{`
`143`	`148`	`code.add_source_location() = loc;`