From 943333a2826e2a99f8e000d1104c08c0fedc04f7 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 11 Nov 2022 13:37:34 +0000
Subject: [PATCH] goto_programt::get_target: fix const-ness of operations

Return a const iterator in a const context to avoid providing a means to
modify instructions in a goto program despite being in a const context.
---
 src/goto-programs/goto_convert.cpp |  2 +-
 src/goto-programs/goto_program.h   | 10 +++++++++-
 2 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index 63e0d793971..b83502cc75f 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -243,7 +243,7 @@ void goto_convertt::optimize_guarded_gotos(goto_programt &dest)
 
   // mark the goto targets
   unsigned cnt = 0;
-  for(const auto &i : dest.instructions)
+  for(auto &i : dest.instructions)
     if(i.is_goto())
       i.get_target()->target_number = (++cnt);
 
diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h
index 76ff252ef4b..49514f40a64 100644
--- a/src/goto-programs/goto_program.h
+++ b/src/goto-programs/goto_program.h
@@ -395,7 +395,15 @@ class goto_programt
 
     /// Returns the first (and only) successor for the usual case of a single
     /// target
-    targett get_target() const
+    const_targett get_target() const
+    {
+      PRECONDITION(targets.size() == 1);
+      return targets.front();
+    }
+
+    /// Returns the first (and only) successor for the usual case of a single
+    /// target
+    targett get_target()
     {
       PRECONDITION(targets.size()==1);
       return targets.front();