add goto_programt::make_return(c, l)

Daniel Kroening · Daniel Kroening · commit 1b2d5d6f34cd · 2019-01-31T08:39:29.000Z
This avoids modification of instructiont::code after the object's creation.
diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h
@@ -814,6 +814,12 @@ class goto_programt
     return instructiont(code_returnt(), irep_idt(), l, RETURN, nil_exprt(), {});
   }
 
+  static instructiont
+  make_return(code_returnt c, const source_locationt &l = source_locationt::nil())
+  {
+    return instructiont(std::move(c), irep_idt(), l, RETURN, nil_exprt(), {});
+  }
+
   static instructiont
   make_skip(const source_locationt &l = source_locationt::nil())
   {

Original file line number	Diff line number	Diff line change
`@@ -814,6 +814,12 @@ class goto_programt`
`814`	`814`	`return instructiont(code_returnt(), irep_idt(), l, RETURN, nil_exprt(), {});`
`815`	`815`	`}`
`816`	`816`
	`817`	`+ static instructiont`
	`818`	`+ make_return(code_returnt c, const source_locationt &l = source_locationt::nil())`
	`819`	`+ {`
	`820`	`+ return instructiont(std::move(c), irep_idt(), l, RETURN, nil_exprt(), {});`
	`821`	`+ }`
	`822`	`+`
`817`	`823`	`static instructiont`
`818`	`824`	`make_skip(const source_locationt &l = source_locationt::nil())`
`819`	`825`	`{`