Address include-what-you-use warnings

More recent versions of iwyu identified new unused headers. (But
struggled to cope with `class C { ... } c;` so that was rewritten as
`class C { ... }; C c;`.)

Author: tautschnig

src/analyses/global_may_alias.h

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_ANALYSES_GLOBAL_MAY_ALIAS_H
 #define CPROVER_ANALYSES_GLOBAL_MAY_ALIAS_H
 
-#include <util/numbering.h>
 #include <util/threeval.h>
 #include <util/union_find.h>
 

src/ansi-c/ansi_c_language.cpp

@@ -23,8 +23,6 @@ Author: Daniel Kroening, [email protected]
 #include "expr2c.h"
 #include "type2name.h"
 
-#include <fstream>
-
 std::set<std::string> ansi_c_languaget::extensions() const
 {
   return { "c", "i" };

src/goto-checker/solver_factory.h

@@ -15,6 +15,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include <solvers/flattening/boolbv.h>
 #include <solvers/smt2/smt2_dec.h>
 
+#include <fstream>
 #include <memory>
 
 class cmdlinet;

src/goto-programs/goto_program.h

@@ -17,7 +17,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_instruction_code.h"
 
-#include <iosfwd>
 #include <limits>
 #include <list>
 #include <set>

src/goto-programs/goto_trace.cpp

@@ -27,8 +27,6 @@ Author: Daniel Kroening
 #include <ansi-c/printf_formatter.h>
 #include <langapi/language_util.h>
 
-#include <ostream>
-
 static std::optional<symbol_exprt> get_object_rec(const exprt &src)
 {
   if(src.id()==ID_symbol)

src/goto-programs/show_goto_functions_json.cpp

@@ -16,8 +16,6 @@ Author: Thomas Kiley
 
 #include "goto_functions.h"
 
-#include <iostream>
-
 /// For outputting the GOTO program in a readable JSON format.
 /// \param _list_only: output only list of functions, but not their bodies
 show_goto_functions_jsont::show_goto_functions_jsont(bool _list_only)

src/goto-programs/show_goto_functions_xml.cpp

@@ -16,8 +16,6 @@ Author: Thomas Kiley
 
 #include "goto_functions.h"
 
-#include <iostream>
-
 /// For outputting the GOTO program in a readable xml format.
 /// \param _list_only: output only list of functions, but not their bodies
 show_goto_functions_xmlt::show_goto_functions_xmlt(bool _list_only)

src/goto-programs/validate_goto_model.h

@@ -10,7 +10,7 @@ Date: Oct 2018
 #ifndef CPROVER_GOTO_PROGRAMS_VALIDATE_GOTO_MODEL_H
 #define CPROVER_GOTO_PROGRAMS_VALIDATE_GOTO_MODEL_H
 
-#include <util/validation_mode.h>
+#include <util/validation_mode.h> // IWYU pragma: keep
 
 class goto_model_validation_optionst final
 {

src/goto-symex/goto_symex_state.h

@@ -26,7 +26,6 @@ Author: Daniel Kroening, [email protected]
 #include "shadow_memory_state.h"
 
 #include <functional>
-#include <memory>
 
 class incremental_dirtyt;
 class symex_target_equationt;

src/pointer-analysis/value_set.cpp

@@ -27,8 +27,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/symbol.h>
 #include <util/xml.h>
 
-#include <ostream>
-
 #ifdef DEBUG
 #include <iostream>
 #include <util/format_expr.h>

src/solvers/sat/dimacs_cnf.cpp

@@ -12,8 +12,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/invariant.h>
 #include <util/magic.h>
 
-#include <iostream>
-
 dimacs_cnft::dimacs_cnft(message_handlert &message_handler)
   : cnf_clause_listt(message_handler), break_lines(false)
 {

src/solvers/smt2/smt2_dec.cpp

@@ -15,6 +15,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "smt2irep.h"
 
+#include <fstream>
+
 std::string smt2_dect::decision_procedure_text() const
 {
   // clang-format off

src/solvers/smt2/smt2_dec.h

@@ -12,8 +12,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "smt2_conv.h"
 
-#include <fstream>
-
 class message_handlert;
 
 class smt2_stringstreamt

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -143,7 +143,8 @@ class smt2_incremental_decision_proceduret final
     {
       return next_id++;
     }
-  } handle_sequence, array_sequence, index_sequence, padding_sequence;
+  };
+  sequencet handle_sequence, array_sequence, index_sequence, padding_sequence;
   /// When the `handle(exprt)` member function is called, the decision procedure
   /// commands the SMT solver to define a new function corresponding to the
   /// given expression. The mapping of the expressions to the function