diffblue · kroening · Jul 17, 2017 · May 7, 2017 · May 7, 2017 · May 7, 2017
diff --git a/CODING_STANDARD.md b/CODING_STANDARD.md
@@ -103,6 +103,10 @@ Here a few minimalistic coding rules for the CPROVER source tree.
 - Prefer forward declaration to includes, but forward declare at the top of the
   header file rather than in line
 - Guard headers with `#ifndef CPROVER_DIRECTORIES_FILE_H`, etc
+- The corresponding header for a given source file should always be the *first*
+  include in the source file. For example, given `foo.h` and `foo.cpp`, the
+  line `#include "foo.h"` should precede all other include statements in
+  `foo.cpp`.
 
 # Makefiles
 - Each source file should appear on a separate line

diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
@@ -9,6 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Abstract Interpretation
 
+#include "ai.h"
+
 #include <cassert>
 #include <memory>
 #include <sstream>
@@ -19,8 +21,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "is_threaded.h"
 
-#include "ai.h"
-
 jsont ai_domain_baset::output_json(
   const ai_baset &ai,
   const namespacet &ns) const

diff --git a/src/analyses/call_graph.cpp b/src/analyses/call_graph.cpp
@@ -9,11 +9,11 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Function Call Graphs
 
+#include "call_graph.h"
+
 #include <util/std_expr.h>
 #include <util/xml.h>
 
-#include "call_graph.h"
-
 call_grapht::call_grapht()
 {
 }

diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
@@ -9,6 +9,8 @@ Author: Peter Schrammel
 /// \file
 /// Constant Propagation
 
+#include "constant_propagator.h"
+
 #ifdef DEBUG
 #include <iostream>
 #endif
@@ -17,8 +19,6 @@ Author: Peter Schrammel
 #include <util/arith_tools.h>
 #include <util/simplify_expr.h>
 
-#include "constant_propagator.h"
-
 exprt concatenate_array_id(
 		const exprt &array, const exprt &index,
 		const typet &type)

diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp
@@ -9,11 +9,11 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Field-insensitive, location-sensitive bitvector analysis
 
+#include "custom_bitvector_analysis.h"
+
 #include <util/xml_expr.h>
 #include <util/simplify_expr.h>
 
-#include "custom_bitvector_analysis.h"
-
 #include <iostream>
 
 void custom_bitvector_domaint::set_bit(

diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp
@@ -12,15 +12,15 @@ Date: August 2013
 /// \file
 /// Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010
 
+#include "dependence_graph.h"
+
 #include <cassert>
 
 #include <util/json.h>
 #include <util/json_expr.h>
 
 #include "goto_rw.h"
 
-#include "dependence_graph.h"
-
 bool dep_graph_domaint::merge(
   const dep_graph_domaint &src,
   goto_programt::const_targett from,

diff --git a/src/analyses/dirty.cpp b/src/analyses/dirty.cpp
@@ -11,10 +11,10 @@ Date: March 2013
 /// \file
 /// Local variables whose address is taken
 
-#include <util/std_expr.h>
-
 #include "dirty.h"
 
+#include <util/std_expr.h>
+
 void dirtyt::build(const goto_functiont &goto_function)
 {
   forall_goto_program_instructions(it, goto_function.body)

diff --git a/src/analyses/does_remove_const.cpp b/src/analyses/does_remove_const.cpp
@@ -9,15 +9,15 @@
 /// \file
 /// Analyses
 
+#include "does_remove_const.h"
+
 #include <goto-programs/goto_program.h>
 #include <util/type.h>
 #include <util/expr.h>
 #include <util/std_code.h>
 #include <util/base_type.h>
 #include <ansi-c/c_qualifiers.h>
 
-#include "does_remove_const.h"
-
 /// A naive analysis to look for casts that remove const-ness from pointers.
 /// \param goto_program: the goto program to check
 /// \param ns: the namespace of the goto program (used for checking type

diff --git a/src/analyses/does_remove_const.h b/src/analyses/does_remove_const.h
@@ -14,6 +14,8 @@
 #include <util/type.h>
 
 class goto_programt;
+class namespacet;
+class exprt;
 
 class does_remove_constt
 {

diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp
@@ -9,10 +9,10 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Field-insensitive, location-sensitive escape analysis
 
-#include <util/simplify_expr.h>
-
 #include "escape_analysis.h"
 
+#include <util/simplify_expr.h>
+
 bool escape_domaint::is_tracked(const symbol_exprt &symbol)
 {
   const irep_idt &identifier=symbol.get_identifier();

diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp
@@ -10,13 +10,13 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Flow Insensitive Static Analysis
 
+#include "flow_insensitive_analysis.h"
+
 #include <cassert>
 
 #include <util/std_expr.h>
 #include <util/std_code.h>
 
-#include "flow_insensitive_analysis.h"
-
 exprt flow_insensitive_abstract_domain_baset::get_guard(
   locationt from,
   locationt to) const

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
@@ -9,6 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// GOTO Programs
 
+#include "goto_check.h"
+
 #include <algorithm>
 
 #include <util/simplify_expr.h>
@@ -27,7 +29,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/options.h>
 
 #include "local_bitvector_analysis.h"
-#include "goto_check.h"
 
 class goto_checkt
 {

diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
@@ -8,6 +8,7 @@ Date: April 2010
 
 \*******************************************************************/
 
+#include "goto_rw.h"
 
 #include <limits>
 #include <algorithm>
@@ -24,8 +25,6 @@ Date: April 2010
 
 #include <pointer-analysis/goto_program_dereference.h>
 
-#include "goto_rw.h"
-
 range_domain_baset::~range_domain_baset()
 {
 }

diff --git a/src/analyses/interval_analysis.cpp b/src/analyses/interval_analysis.cpp
@@ -9,10 +9,11 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Interval Analysis
 
+#include "interval_analysis.h"
+
 #include <util/find_symbols.h>
 
 #include "interval_domain.h"
-#include "interval_analysis.h"
 
 void instrument_intervals(
   const ait<interval_domaint> &interval_analysis,

diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp
@@ -9,6 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Interval Domain
 
+#include "interval_domain.h"
+
 #ifdef DEBUG
 #include <iostream>
 #endif
@@ -17,8 +19,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/arith_tools.h>
 
-#include "interval_domain.h"
-
 void interval_domaint::output(
   std::ostream &out,
   const ai_baset &ai,

diff --git a/src/analyses/invariant_propagation.cpp b/src/analyses/invariant_propagation.cpp
@@ -9,13 +9,13 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Invariant Propagation
 
+#include "invariant_propagation.h"
+
 #include <util/simplify_expr.h>
 #include <util/base_type.h>
 #include <util/symbol_table.h>
 #include <util/std_expr.h>
 
-#include "invariant_propagation.h"
-
 void invariant_propagationt::make_all_true()
 {
   for(auto &state : state_map)

diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp
@@ -9,6 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Invariant Set
 
+#include "invariant_set.h"
+
 #include <iostream>
 
 #include <util/symbol_table.h>
@@ -22,8 +24,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <langapi/language_util.h>
 
-#include "invariant_set.h"
-
 void inv_object_storet::output(std::ostream &out) const
 {
   for(unsigned i=0; i<entries.size(); i++)

diff --git a/src/analyses/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp
@@ -9,10 +9,10 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Invariant Set Domain
 
-#include <util/simplify_expr.h>
-
 #include "invariant_set_domain.h"
 
+#include <util/simplify_expr.h>
+
 void invariant_set_domaint::transform(
   locationt from_l,
   locationt to_l,

diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp
@@ -11,9 +11,10 @@ Date: October 2012
 /// \file
 /// Over-approximate Concurrency for Threaded Goto Programs
 
-#include "ai.h"
 #include "is_threaded.h"
 
+#include "ai.h"
+
 class is_threaded_domaint:public ai_domain_baset
 {
 public:

diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp
@@ -9,6 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Field-insensitive, location-sensitive may-alias analysis
 
+#include "local_bitvector_analysis.h"
+
 #include <iterator>
 #include <algorithm>
 
@@ -19,8 +21,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <langapi/language_util.h>
 
-#include "local_bitvector_analysis.h"
-
 void local_bitvector_analysist::flagst::print(std::ostream &out) const
 {
   if(is_unknown())

diff --git a/src/analyses/local_cfg.cpp b/src/analyses/local_cfg.cpp
@@ -9,6 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// CFG for One Function
 
+#include "local_cfg.h"
+
 #if 0
 #include <iterator>
 #include <algorithm>
@@ -22,8 +24,6 @@ Author: Daniel Kroening, [email protected]
 
 #endif
 
-#include "local_cfg.h"
-
 void local_cfgt::build(const goto_programt &goto_program)
 {
   nodes.resize(goto_program.instructions.size());

diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp
@@ -9,6 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Field-insensitive, location-sensitive may-alias analysis
 
+#include "local_may_alias.h"
+
 #include <iterator>
 #include <algorithm>
 
@@ -19,8 +21,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <langapi/language_util.h>
 
-#include "local_may_alias.h"
-
 /// \return return 'true' iff changed
 bool local_may_aliast::loc_infot::merge(const loc_infot &src)
 {

diff --git a/src/analyses/locals.cpp b/src/analyses/locals.cpp
@@ -11,10 +11,10 @@ Date: March 2013
 /// \file
 /// Local variables
 
-#include <util/std_expr.h>
-
 #include "locals.h"
 
+#include <util/std_expr.h>
+
 void localst::build(const goto_functiont &goto_function)
 {
   forall_goto_program_instructions(it, goto_function.body)

diff --git a/src/analyses/natural_loops.cpp b/src/analyses/natural_loops.cpp
@@ -9,10 +9,10 @@ Author: Georg Weissenbacher, [email protected]
 /// \file
 /// Dominators
 
-#include <iostream>
-
 #include "natural_loops.h"
 
+#include <iostream>
+
 void show_natural_loops(const goto_functionst &goto_functions)
 {
   forall_goto_functions(it, goto_functions)

diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp
@@ -13,6 +13,8 @@ Date: February 2013
 /// Range-based reaching definitions analysis (following Field- Sensitive
 ///   Program Dependence Analysis, Litvak et al., FSE 2010)
 
+#include "reaching_definitions.h"
+
 #include <util/pointer_offset_size.h>
 #include <util/prefix.h>
 
@@ -21,8 +23,6 @@ Date: February 2013
 #include "is_threaded.h"
 #include "dirty.h"
 
-#include "reaching_definitions.h"
-
 void rd_range_domaint::populate_cache(const irep_idt &identifier) const
 {
   assert(bv_container);

diff --git a/src/analyses/replace_symbol_ext.cpp b/src/analyses/replace_symbol_ext.cpp
@@ -9,11 +9,11 @@ Author: Peter Schrammel
 /// \file
 /// Modified expression replacement for constant propagator
 
+#include "replace_symbol_ext.h"
+
 #include <util/std_types.h>
 #include <util/std_expr.h>
 
-#include "replace_symbol_ext.h"
-
 /// does not replace object in address_of expressions
 bool replace_symbol_extt::replace(exprt &dest) const
 {