Make path_nodet.output const

janmroczkowski · janmroczkowski · commit 211fcc225eb8 · 2017-09-06T18:29:14.000+01:00
diff --git a/src/goto-instrument/accelerate/path.h b/src/goto-instrument/accelerate/path.h
@@ -36,7 +36,7 @@ class path_nodet
   {
   }
 
-  void output(const goto_programt &program, std::ostream &str);
+  void output(const goto_programt &program, std::ostream &str) const;
 
   goto_programt::targett loc;
   const exprt guard;

Original file line number	Diff line number	Diff line change
`@@ -36,7 +36,7 @@ class path_nodet`
`36`	`36`	`{`
`37`	`37`	`}`
`38`	`38`
`39`		`- void output(const goto_programt &program, std::ostream &str);`
	`39`	`+ void output(const goto_programt &program, std::ostream &str) const;`
`40`	`40`
`41`	`41`	`goto_programt::targett loc;`
`42`	`42`	`const exprt guard;`