CONTRACTS: havoc_utilst methods are now non-const

To support slice operators in loop assigns clauses
the methods need to be non-const, since havocing
a slice using havoc_slice will modify the symbol table.

Author: Remi Delmas

src/goto-instrument/havoc_utils.cpp

@@ -20,7 +20,7 @@ Date: July 2021
 
 void havoc_utilst::append_full_havoc_code(
   const source_locationt location,
-  goto_programt &dest) const
+  goto_programt &dest)
 {
   for(const auto &expr : assigns)
     append_havoc_code_for_expr(location, expr, dest);
@@ -29,7 +29,7 @@ void havoc_utilst::append_full_havoc_code(
 void havoc_utilst::append_havoc_code_for_expr(
   const source_locationt location,
   const exprt &expr,
-  goto_programt &dest) const
+  goto_programt &dest)
 {
   if(expr.id() == ID_index || expr.id() == ID_dereference)
   {

src/goto-instrument/havoc_utils.h

@@ -60,7 +60,7 @@ class havoc_utilst
   /// \param dest The destination goto program to append the instructions to
   void append_full_havoc_code(
     const source_locationt location,
-    goto_programt &dest) const;
+    goto_programt &dest);
 
   /// \brief Append goto instructions to havoc a single expression `expr`
   ///
@@ -76,7 +76,7 @@ class havoc_utilst
   virtual void append_havoc_code_for_expr(
     const source_locationt location,
     const exprt &expr,
-    goto_programt &dest) const;
+    goto_programt &dest);
 
   /// \brief Append goto instructions to havoc the underlying object of `expr`
   ///