From d6986d8fa0edb24a5c689989af3a2f473983de4c Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Thu, 17 May 2018 21:56:08 +0100
Subject: [PATCH 1/4] Fix relative include paths

---
 src/ansi-c/literals/convert_float_literal.cpp    | 3 ++-
 src/goto-instrument/wmm/goto2graph.cpp           | 3 ++-
 src/goto-instrument/wmm/shared_buffers.cpp       | 3 ++-
 src/goto-instrument/wmm/weak_memory.cpp          | 2 +-
 src/solvers/flattening/boolbv.cpp                | 4 ++--
 src/solvers/flattening/boolbv_abs.cpp            | 2 +-
 src/solvers/flattening/boolbv_add_sub.cpp        | 2 +-
 src/solvers/flattening/boolbv_bv_rel.cpp         | 2 +-
 src/solvers/flattening/boolbv_floatbv_op.cpp     | 2 +-
 src/solvers/flattening/boolbv_ieee_float_rel.cpp | 2 +-
 src/solvers/flattening/boolbv_map.cpp            | 2 +-
 src/solvers/flattening/boolbv_typecast.cpp       | 4 ++--
 src/solvers/flattening/boolbv_unary_minus.cpp    | 4 ++--
 src/solvers/floatbv/float_bv.h                   | 2 +-
 src/solvers/qbf/qdimacs_cnf.h                    | 2 +-
 15 files changed, 21 insertions(+), 18 deletions(-)

diff --git a/src/ansi-c/literals/convert_float_literal.cpp b/src/ansi-c/literals/convert_float_literal.cpp
index a7e817c82f5..35599d1bf7d 100644
--- a/src/ansi-c/literals/convert_float_literal.cpp
+++ b/src/ansi-c/literals/convert_float_literal.cpp
@@ -21,8 +21,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_types.h>
 #include <util/string2int.h>
 
+#include <ansi-c/gcc_types.h>
+
 #include "parse_float.h"
-#include "../gcc_types.h"
 
 exprt convert_float_literal(const std::string &src)
 {
diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp
index 6d130be954b..e29d78d6b46 100644
--- a/src/goto-instrument/wmm/goto2graph.cpp
+++ b/src/goto-instrument/wmm/goto2graph.cpp
@@ -21,7 +21,8 @@ Date: 2012
 
 #include <linking/static_lifetime_init.h>
 
-#include "../rw_set.h"
+#include <goto-instrument/rw_set.h>
+
 #include "fence.h"
 
 // #define PRINT_UNSAFES
diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp
index feadf6af1ad..05c339c2117 100644
--- a/src/goto-instrument/wmm/shared_buffers.cpp
+++ b/src/goto-instrument/wmm/shared_buffers.cpp
@@ -12,7 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <linking/static_lifetime_init.h>
 
-#include "../rw_set.h"
+#include <goto-instrument/rw_set.h>
+
 #include "fence.h"
 
 /// returns a unique id (for fresh variables)
diff --git a/src/goto-instrument/wmm/weak_memory.cpp b/src/goto-instrument/wmm/weak_memory.cpp
index 155e2064383..aa2a316be97 100644
--- a/src/goto-instrument/wmm/weak_memory.cpp
+++ b/src/goto-instrument/wmm/weak_memory.cpp
@@ -27,7 +27,7 @@ Date: September 2011
 
 #include <linking/static_lifetime_init.h>
 
-#include "../rw_set.h"
+#include <goto-instrument/rw_set.h>
 
 #include "shared_buffers.h"
 #include "goto2graph.h"
diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index 40ddc83e3d6..adc20b6144f 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/src/solvers/flattening/boolbv.cpp
@@ -26,8 +26,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv_type.h"
 
-#include "../floatbv/float_utils.h"
-#include "../lowering/expr_lowering.h"
+#include <solvers/floatbv/float_utils.h>
+#include <solvers/lowering/expr_lowering.h>
 
 bool boolbvt::literal(
   const exprt &expr,
diff --git a/src/solvers/flattening/boolbv_abs.cpp b/src/solvers/flattening/boolbv_abs.cpp
index 7f10b724ed1..1caabde0fa4 100644
--- a/src/solvers/flattening/boolbv_abs.cpp
+++ b/src/solvers/flattening/boolbv_abs.cpp
@@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv_type.h"
 
-#include "../floatbv/float_utils.h"
+#include <solvers/floatbv/float_utils.h>
 
 bvt boolbvt::convert_abs(const exprt &expr)
 {
diff --git a/src/solvers/flattening/boolbv_add_sub.cpp b/src/solvers/flattening/boolbv_add_sub.cpp
index fc4e66935d9..3656b33384a 100644
--- a/src/solvers/flattening/boolbv_add_sub.cpp
+++ b/src/solvers/flattening/boolbv_add_sub.cpp
@@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/invariant.h>
 #include <util/std_types.h>
 
-#include "../floatbv/float_utils.h"
+#include <solvers/floatbv/float_utils.h>
 
 bvt boolbvt::convert_add_sub(const exprt &expr)
 {
diff --git a/src/solvers/flattening/boolbv_bv_rel.cpp b/src/solvers/flattening/boolbv_bv_rel.cpp
index 37f3dbadd3c..86140972cd2 100644
--- a/src/solvers/flattening/boolbv_bv_rel.cpp
+++ b/src/solvers/flattening/boolbv_bv_rel.cpp
@@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv_type.h"
 
-#include "../floatbv/float_utils.h"
+#include <solvers/floatbv/float_utils.h>
 
 literalt boolbvt::convert_bv_rel(const exprt &expr)
 {
diff --git a/src/solvers/flattening/boolbv_floatbv_op.cpp b/src/solvers/flattening/boolbv_floatbv_op.cpp
index 6f5b762c17d..8a7bf6f0a28 100644
--- a/src/solvers/flattening/boolbv_floatbv_op.cpp
+++ b/src/solvers/flattening/boolbv_floatbv_op.cpp
@@ -13,7 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/std_types.h>
 
-#include "../floatbv/float_utils.h"
+#include <solvers/floatbv/float_utils.h>
 
 bvt boolbvt::convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
 {
diff --git a/src/solvers/flattening/boolbv_ieee_float_rel.cpp b/src/solvers/flattening/boolbv_ieee_float_rel.cpp
index c7297d26792..87c86572e0d 100644
--- a/src/solvers/flattening/boolbv_ieee_float_rel.cpp
+++ b/src/solvers/flattening/boolbv_ieee_float_rel.cpp
@@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv_type.h"
 
-#include "../floatbv/float_utils.h"
+#include <solvers/floatbv/float_utils.h>
 
 literalt boolbvt::convert_ieee_float_rel(const exprt &expr)
 {
diff --git a/src/solvers/flattening/boolbv_map.cpp b/src/solvers/flattening/boolbv_map.cpp
index f9dc4fa9a16..fd12b81ebd7 100644
--- a/src/solvers/flattening/boolbv_map.cpp
+++ b/src/solvers/flattening/boolbv_map.cpp
@@ -10,7 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/threeval.h>
 
-#include "../prop/prop.h"
+#include <solvers/prop/prop.h>
 
 #include "boolbv_width.h"
 
diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp
index ecd2522532c..838c8df84ac 100644
--- a/src/solvers/flattening/boolbv_typecast.cpp
+++ b/src/solvers/flattening/boolbv_typecast.cpp
@@ -12,11 +12,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/std_types.h>
 
+#include <solvers/floatbv/float_utils.h>
+
 #include "boolbv_type.h"
 #include "c_bit_field_replacement_type.h"
 
-#include "../floatbv/float_utils.h"
-
 bvt boolbvt::convert_bv_typecast(const typecast_exprt &expr)
 {
   const typet &expr_type=ns.follow(expr.type());
diff --git a/src/solvers/flattening/boolbv_unary_minus.cpp b/src/solvers/flattening/boolbv_unary_minus.cpp
index e4b2707c108..05424f29914 100644
--- a/src/solvers/flattening/boolbv_unary_minus.cpp
+++ b/src/solvers/flattening/boolbv_unary_minus.cpp
@@ -10,9 +10,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/std_types.h>
 
-#include "boolbv_type.h"
+#include <solvers/floatbv/float_utils.h>
 
-#include "../floatbv/float_utils.h"
+#include "boolbv_type.h"
 
 bvt boolbvt::convert_unary_minus(const unary_exprt &expr)
 {
diff --git a/src/solvers/floatbv/float_bv.h b/src/solvers/floatbv/float_bv.h
index f9a58ba2695..9c071b73e33 100644
--- a/src/solvers/floatbv/float_bv.h
+++ b/src/solvers/floatbv/float_bv.h
@@ -13,7 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/ieee_float.h>
 #include <util/std_expr.h>
 
-#include "../flattening/bv_utils.h"
+#include <solvers/flattening/bv_utils.h>
 
 class float_bvt
 {
diff --git a/src/solvers/qbf/qdimacs_cnf.h b/src/solvers/qbf/qdimacs_cnf.h
index d96c69300bd..7cecbb90c1d 100644
--- a/src/solvers/qbf/qdimacs_cnf.h
+++ b/src/solvers/qbf/qdimacs_cnf.h
@@ -13,7 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <set>
 #include <iosfwd>
 
-#include "../sat/dimacs_cnf.h"
+#include <solvers/sat/dimacs_cnf.h>
 
 class qdimacs_cnft:public dimacs_cnft
 {

From 88f8cfc3266745742268fa6b42f0b92021f69bac Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Mon, 21 May 2018 17:18:31 +0100
Subject: [PATCH 2/4] Remove unnecessary includes

---
 jbmc/src/janalyzer/janalyzer_parse_options.cpp | 2 --
 1 file changed, 2 deletions(-)

diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
index 1aa6b69ad69..21c93527c0a 100644
--- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp
+++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
@@ -17,9 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <memory>
 
 #include <ansi-c/ansi_c_language.h>
-#include <cpp/cpp_language.h>
 #include <java_bytecode/java_bytecode_language.h>
-#include <jsil/jsil_language.h>
 
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_inline.h>

From a90ea445a529ad48e2ad8da783cbd3d3d3b0f06b Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Thu, 17 May 2018 17:35:16 +0100
Subject: [PATCH 3/4] Add module dependency check to CPP-LINT

To use it just put a module_dependencies.txt into a directory,
which lists all modules that it is allowed to include header
files from.
---
 scripts/cpplint.py | 45 +++++++++++++++++++++++++++++++++++++++------
 1 file changed, 39 insertions(+), 6 deletions(-)

diff --git a/scripts/cpplint.py b/scripts/cpplint.py
index b42395158e9..242a320ff0d 100755
--- a/scripts/cpplint.py
+++ b/scripts/cpplint.py
@@ -4981,7 +4981,7 @@ def _ClassifyInclude(fileinfo, include, is_system):
 
 
 
-def CheckIncludeLine(filename, clean_lines, linenum, include_state, error):
+def CheckIncludeLine(filename, clean_lines, linenum, include_state, error, module_deps):
   """Check rules that are applicable to #include lines.
 
   Strings on #include lines are NOT removed from elided line, to make
@@ -5029,6 +5029,18 @@ def CheckIncludeLine(filename, clean_lines, linenum, include_state, error):
     elif not _THIRD_PARTY_HEADERS_PATTERN.match(include):
       include_state.include_list[-1].append((include, linenum))
 
+    # Check module dependencies
+    module_name = os.path.dirname(filename)
+    has_src = module_name.find('src/')
+    if has_src >= 0:
+        module_name = module_name[has_src+4:]
+    deps_name = os.path.dirname(include)
+    if deps_name and module_deps:
+        may_use = any(deps_name.startswith(module) for module in module_deps)
+        if not may_use:
+            error(filename, linenum, 'build/include', 4,
+                  'Module `'+module_name+'` must not use `'+include+'`')
+
       # We want to ensure that headers appear in the right order:
       # 1) for foo.cc, foo.h  (preferred location)
       # 2) c system files
@@ -5141,7 +5153,7 @@ def _GetTextInside(text, start_pattern):
 
 
 def CheckLanguage(filename, clean_lines, linenum, file_extension,
-                  include_state, nesting_state, error):
+                  include_state, nesting_state, error, module_deps):
   """Checks rules from the 'C++ language rules' section of cppguide.html.
 
   Some of these rules are hard to test (function overloading, using
@@ -5165,7 +5177,7 @@ def CheckLanguage(filename, clean_lines, linenum, file_extension,
 
   match = _RE_PATTERN_INCLUDE.search(line)
   if match:
-    CheckIncludeLine(filename, clean_lines, linenum, include_state, error)
+    CheckIncludeLine(filename, clean_lines, linenum, include_state, error, module_deps)
     return
 
   # Reset include state across preprocessor directives.  This is meant
@@ -6246,7 +6258,7 @@ def CheckForEndl(filename, clean_lines, linenum, error):
     error(filename, linenum, 'runtime/endl', 4, 'Do not use std::endl')
 
 def ProcessLine(filename, file_extension, clean_lines, line,
-                include_state, function_state, nesting_state, error,
+                include_state, function_state, nesting_state, error, module_deps,
                 extra_check_functions=[]):
   """Processes a single line in the file.
 
@@ -6276,7 +6288,7 @@ def ProcessLine(filename, file_extension, clean_lines, line,
   CheckForMultilineCommentsAndStrings(filename, clean_lines, line, error)
   CheckStyle(filename, clean_lines, line, file_extension, nesting_state, error)
   CheckLanguage(filename, clean_lines, line, file_extension, include_state,
-                nesting_state, error)
+                nesting_state, error, module_deps)
   CheckForNonConstReference(filename, clean_lines, line, nesting_state, error)
   CheckForNonStandardConstructs(filename, clean_lines, line,
                                 nesting_state, error)
@@ -6370,6 +6382,27 @@ def ProcessFileData(filename, file_extension, lines, error,
 
   ResetNolintSuppressions()
 
+  # Load module dependencies
+  module_deps_file = os.path.join(os.path.dirname(filename), 'module_dependencies.txt')
+  module_deps = []
+  if os.path.isfile(module_deps_file):
+      with open(module_deps_file, 'r') as f:
+          module_deps = f.read().splitlines()
+      # strip off comments and whitespace
+      def strip_off_comments(s):
+          comment_index = s.find('#')
+          if comment_index >= 0:
+              s = s[:comment_index]
+          s = s.strip()
+          return s
+      module_deps = [strip_off_comments(module) for module in module_deps]
+      # remove empty lines
+      module_deps = [module for module in module_deps if len(module) != 0]
+  else:
+      error(filename, 0, 'build/include', 4,
+            'module_dependencies.txt not found in `' +
+                os.path.dirname(filename) + '`')
+
   CheckForCopyright(filename, lines, error)
   CheckForFunctionCommentHeaders(filename, lines, error)
   ProcessGlobalSuppresions(lines)
@@ -6381,7 +6414,7 @@ def ProcessFileData(filename, file_extension, lines, error,
 
   for line in xrange(clean_lines.NumLines()):
     ProcessLine(filename, file_extension, clean_lines, line,
-                include_state, function_state, nesting_state, error,
+                include_state, function_state, nesting_state, error, module_deps,
                 extra_check_functions)
     FlagCxx11Features(filename, clean_lines, line, error)
   nesting_state.CheckCompletedBlocks(filename, error)

From fada0afb0c60af7160879e707e0af48a4733a12b Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Thu, 17 May 2018 18:14:40 +0100
Subject: [PATCH 4/4] Add module dependency definition files

---
 jbmc/src/janalyzer/module_dependencies.txt          |  9 +++++++++
 .../java_bytecode/library/module_dependencies.txt   |  1 +
 jbmc/src/java_bytecode/module_dependencies.txt      | 10 ++++++++++
 jbmc/src/jbmc/module_dependencies.txt               | 12 ++++++++++++
 jbmc/src/jdiff/module_dependencies.txt              | 11 +++++++++++
 jbmc/src/miniz/module_dependencies.txt              |  2 ++
 src/analyses/module_dependencies.txt                |  6 ++++++
 src/ansi-c/library/module_dependencies.txt          |  2 ++
 src/ansi-c/literals/module_dependencies.txt         |  3 +++
 src/ansi-c/module_dependencies.txt                  |  6 ++++++
 src/assembler/module_dependencies.txt               |  2 ++
 src/big-int/module_dependencies.txt                 |  1 +
 src/cbmc/module_dependencies.txt                    | 13 +++++++++++++
 src/clobber/module_dependencies.txt                 | 10 ++++++++++
 src/cpp/module_dependencies.txt                     |  5 +++++
 src/goto-analyzer/module_dependencies.txt           | 11 +++++++++++
 src/goto-cc/module_dependencies.txt                 | 10 ++++++++++
 src/goto-diff/module_dependencies.txt               | 12 ++++++++++++
 .../accelerate/module_dependencies.txt              |  7 +++++++
 src/goto-instrument/module_dependencies.txt         | 12 ++++++++++++
 src/goto-instrument/wmm/module_dependencies.txt     |  5 +++++
 src/goto-programs/module_dependencies.txt           | 11 +++++++++++
 src/goto-symex/module_dependencies.txt              |  8 ++++++++
 src/jsil/module_dependencies.txt                    |  6 ++++++
 src/json/module_dependencies.txt                    |  2 ++
 src/langapi/module_dependencies.txt                 |  3 +++
 src/linking/module_dependencies.txt                 |  5 +++++
 src/memory-models/module_dependencies.txt           |  4 ++++
 src/miniz/module_dependencies.txt                   |  2 ++
 src/nonstd/module_dependencies.txt                  |  1 +
 src/pointer-analysis/module_dependencies.txt        |  6 ++++++
 src/solvers/cvc/module_dependencies.txt             |  4 ++++
 src/solvers/flattening/module_dependencies.txt      |  6 ++++++
 src/solvers/floatbv/module_dependencies.txt         |  3 +++
 src/solvers/lowering/module_dependencies.txt        |  2 ++
 src/solvers/miniBDD/module_dependencies.txt         |  1 +
 src/solvers/module_dependencies.txt                 |  1 +
 src/solvers/prop/module_dependencies.txt            |  3 +++
 src/solvers/qbf/module_dependencies.txt             |  5 +++++
 src/solvers/refinement/module_dependencies.txt      |  6 ++++++
 src/solvers/sat/module_dependencies.txt             |  7 +++++++
 src/solvers/smt2/module_dependencies.txt            |  6 ++++++
 src/util/module_dependencies.txt                    |  7 +++++++
 src/xmllang/module_dependencies.txt                 |  2 ++
 44 files changed, 251 insertions(+)
 create mode 100644 jbmc/src/janalyzer/module_dependencies.txt
 create mode 100644 jbmc/src/java_bytecode/library/module_dependencies.txt
 create mode 100644 jbmc/src/java_bytecode/module_dependencies.txt
 create mode 100644 jbmc/src/jbmc/module_dependencies.txt
 create mode 100644 jbmc/src/jdiff/module_dependencies.txt
 create mode 100644 jbmc/src/miniz/module_dependencies.txt
 create mode 100644 src/analyses/module_dependencies.txt
 create mode 100644 src/ansi-c/library/module_dependencies.txt
 create mode 100644 src/ansi-c/literals/module_dependencies.txt
 create mode 100644 src/ansi-c/module_dependencies.txt
 create mode 100644 src/assembler/module_dependencies.txt
 create mode 100644 src/big-int/module_dependencies.txt
 create mode 100644 src/cbmc/module_dependencies.txt
 create mode 100644 src/clobber/module_dependencies.txt
 create mode 100644 src/cpp/module_dependencies.txt
 create mode 100644 src/goto-analyzer/module_dependencies.txt
 create mode 100644 src/goto-cc/module_dependencies.txt
 create mode 100644 src/goto-diff/module_dependencies.txt
 create mode 100644 src/goto-instrument/accelerate/module_dependencies.txt
 create mode 100644 src/goto-instrument/module_dependencies.txt
 create mode 100644 src/goto-instrument/wmm/module_dependencies.txt
 create mode 100644 src/goto-programs/module_dependencies.txt
 create mode 100644 src/goto-symex/module_dependencies.txt
 create mode 100644 src/jsil/module_dependencies.txt
 create mode 100644 src/json/module_dependencies.txt
 create mode 100644 src/langapi/module_dependencies.txt
 create mode 100644 src/linking/module_dependencies.txt
 create mode 100644 src/memory-models/module_dependencies.txt
 create mode 100644 src/miniz/module_dependencies.txt
 create mode 100644 src/nonstd/module_dependencies.txt
 create mode 100644 src/pointer-analysis/module_dependencies.txt
 create mode 100644 src/solvers/cvc/module_dependencies.txt
 create mode 100644 src/solvers/flattening/module_dependencies.txt
 create mode 100644 src/solvers/floatbv/module_dependencies.txt
 create mode 100644 src/solvers/lowering/module_dependencies.txt
 create mode 100644 src/solvers/miniBDD/module_dependencies.txt
 create mode 100644 src/solvers/module_dependencies.txt
 create mode 100644 src/solvers/prop/module_dependencies.txt
 create mode 100644 src/solvers/qbf/module_dependencies.txt
 create mode 100644 src/solvers/refinement/module_dependencies.txt
 create mode 100644 src/solvers/sat/module_dependencies.txt
 create mode 100644 src/solvers/smt2/module_dependencies.txt
 create mode 100644 src/util/module_dependencies.txt
 create mode 100644 src/xmllang/module_dependencies.txt

diff --git a/jbmc/src/janalyzer/module_dependencies.txt b/jbmc/src/janalyzer/module_dependencies.txt
new file mode 100644
index 00000000000..cc11b9898b7
--- /dev/null
+++ b/jbmc/src/janalyzer/module_dependencies.txt
@@ -0,0 +1,9 @@
+analyses
+ansi-c # should go away
+cbmc # version.h
+java_bytecode
+jdiff
+goto-analyzer
+goto-programs
+langapi # should go away
+util
diff --git a/jbmc/src/java_bytecode/library/module_dependencies.txt b/jbmc/src/java_bytecode/library/module_dependencies.txt
new file mode 100644
index 00000000000..ab5e0cc6c7e
--- /dev/null
+++ b/jbmc/src/java_bytecode/library/module_dependencies.txt
@@ -0,0 +1 @@
+java_bytecode/library
diff --git a/jbmc/src/java_bytecode/module_dependencies.txt b/jbmc/src/java_bytecode/module_dependencies.txt
new file mode 100644
index 00000000000..f011bcc8b52
--- /dev/null
+++ b/jbmc/src/java_bytecode/module_dependencies.txt
@@ -0,0 +1,10 @@
+analyses
+ansi-c # should go away
+goto-programs
+java_bytecode
+json
+langapi # should go away
+library
+linking
+miniz
+util
diff --git a/jbmc/src/jbmc/module_dependencies.txt b/jbmc/src/jbmc/module_dependencies.txt
new file mode 100644
index 00000000000..76529547422
--- /dev/null
+++ b/jbmc/src/jbmc/module_dependencies.txt
@@ -0,0 +1,12 @@
+analyses
+ansi-c # should go away
+cbmc # version.h and bmc.h
+goto-instrument
+goto-programs
+goto-symex
+java_bytecode
+jbmc
+langapi # should go away
+linking
+pointer-analysis
+util
diff --git a/jbmc/src/jdiff/module_dependencies.txt b/jbmc/src/jdiff/module_dependencies.txt
new file mode 100644
index 00000000000..5c97868ddf1
--- /dev/null
+++ b/jbmc/src/jdiff/module_dependencies.txt
@@ -0,0 +1,11 @@
+analyses
+cbmc # version.h
+java_bytecode
+jdiff
+goto-diff
+goto-instrument
+goto-programs
+goto-symex # dubious - rewrite_union
+langapi # should go away
+pointer-analysis
+util
diff --git a/jbmc/src/miniz/module_dependencies.txt b/jbmc/src/miniz/module_dependencies.txt
new file mode 100644
index 00000000000..d415f87922b
--- /dev/null
+++ b/jbmc/src/miniz/module_dependencies.txt
@@ -0,0 +1,2 @@
+miniz
+sys # system
diff --git a/src/analyses/module_dependencies.txt b/src/analyses/module_dependencies.txt
new file mode 100644
index 00000000000..8962462ddc2
--- /dev/null
+++ b/src/analyses/module_dependencies.txt
@@ -0,0 +1,6 @@
+analyses
+ansi-c # should go away
+goto-programs
+langapi # should go away
+pointer-analysis
+util
diff --git a/src/ansi-c/library/module_dependencies.txt b/src/ansi-c/library/module_dependencies.txt
new file mode 100644
index 00000000000..646fc1e7b82
--- /dev/null
+++ b/src/ansi-c/library/module_dependencies.txt
@@ -0,0 +1,2 @@
+ansi-c
+ansi-c/library
diff --git a/src/ansi-c/literals/module_dependencies.txt b/src/ansi-c/literals/module_dependencies.txt
new file mode 100644
index 00000000000..014aedd0442
--- /dev/null
+++ b/src/ansi-c/literals/module_dependencies.txt
@@ -0,0 +1,3 @@
+ansi-c
+ansi-c/literals
+util
diff --git a/src/ansi-c/module_dependencies.txt b/src/ansi-c/module_dependencies.txt
new file mode 100644
index 00000000000..466503d3caf
--- /dev/null
+++ b/src/ansi-c/module_dependencies.txt
@@ -0,0 +1,6 @@
+ansi-c
+goto-programs
+langapi # should go away
+linking
+literals
+util
diff --git a/src/assembler/module_dependencies.txt b/src/assembler/module_dependencies.txt
new file mode 100644
index 00000000000..b3f6e3a4261
--- /dev/null
+++ b/src/assembler/module_dependencies.txt
@@ -0,0 +1,2 @@
+assembler
+util
diff --git a/src/big-int/module_dependencies.txt b/src/big-int/module_dependencies.txt
new file mode 100644
index 00000000000..c7e4588006c
--- /dev/null
+++ b/src/big-int/module_dependencies.txt
@@ -0,0 +1 @@
+big-int
diff --git a/src/cbmc/module_dependencies.txt b/src/cbmc/module_dependencies.txt
new file mode 100644
index 00000000000..57d634ccfd7
--- /dev/null
+++ b/src/cbmc/module_dependencies.txt
@@ -0,0 +1,13 @@
+analyses
+ansi-c
+cpp
+goto-instrument
+goto-programs
+goto-symex
+jsil
+langapi # should go away
+linking
+pointer-analysis
+solvers
+xmllang
+util
diff --git a/src/clobber/module_dependencies.txt b/src/clobber/module_dependencies.txt
new file mode 100644
index 00000000000..3ad32b39034
--- /dev/null
+++ b/src/clobber/module_dependencies.txt
@@ -0,0 +1,10 @@
+analyses
+ansi-c
+cbmc
+clobber
+cpp
+goto-programs
+goto-instrument
+java_bytecode # will go away
+langapi # should go away
+util
diff --git a/src/cpp/module_dependencies.txt b/src/cpp/module_dependencies.txt
new file mode 100644
index 00000000000..8bd4b3854cf
--- /dev/null
+++ b/src/cpp/module_dependencies.txt
@@ -0,0 +1,5 @@
+ansi-c
+cpp
+langapi # should go away
+linking
+util
diff --git a/src/goto-analyzer/module_dependencies.txt b/src/goto-analyzer/module_dependencies.txt
new file mode 100644
index 00000000000..e3ad5a094da
--- /dev/null
+++ b/src/goto-analyzer/module_dependencies.txt
@@ -0,0 +1,11 @@
+ansi-c
+analyses
+cbmc # version.h
+cpp
+goto-analyzer
+goto-programs
+java_bytecode # will go away
+langapi # should go away
+jsil
+json
+util
diff --git a/src/goto-cc/module_dependencies.txt b/src/goto-cc/module_dependencies.txt
new file mode 100644
index 00000000000..6d867541014
--- /dev/null
+++ b/src/goto-cc/module_dependencies.txt
@@ -0,0 +1,10 @@
+ansi-c
+cbmc # version.h
+cpp
+goto-cc
+goto-programs
+jsil
+json
+langapi # should go away
+linking
+util
diff --git a/src/goto-diff/module_dependencies.txt b/src/goto-diff/module_dependencies.txt
new file mode 100644
index 00000000000..cd004e5e879
--- /dev/null
+++ b/src/goto-diff/module_dependencies.txt
@@ -0,0 +1,12 @@
+analyses
+ansi-c
+cbmc # version.h
+cpp
+goto-diff
+goto-instrument
+goto-programs
+goto-symex # dubious - rewrite_union and adjust_float should be moved to goto-programs
+java_bytecode # will go away
+langapi # should go away
+pointer-analysis
+util
diff --git a/src/goto-instrument/accelerate/module_dependencies.txt b/src/goto-instrument/accelerate/module_dependencies.txt
new file mode 100644
index 00000000000..f19043cbc94
--- /dev/null
+++ b/src/goto-instrument/accelerate/module_dependencies.txt
@@ -0,0 +1,7 @@
+analyses
+ansi-c # should go away
+goto-instrument/accelerate
+goto-programs
+goto-symex
+solvers
+util
diff --git a/src/goto-instrument/module_dependencies.txt b/src/goto-instrument/module_dependencies.txt
new file mode 100644
index 00000000000..44bc38028be
--- /dev/null
+++ b/src/goto-instrument/module_dependencies.txt
@@ -0,0 +1,12 @@
+accelerate
+analyses
+ansi-c
+cbmc # version.h
+cpp
+goto-instrument
+goto-programs
+langapi # should go away
+linking
+pointer-analysis
+util
+wmm
diff --git a/src/goto-instrument/wmm/module_dependencies.txt b/src/goto-instrument/wmm/module_dependencies.txt
new file mode 100644
index 00000000000..b9d05734214
--- /dev/null
+++ b/src/goto-instrument/wmm/module_dependencies.txt
@@ -0,0 +1,5 @@
+goto-instrument
+goto-instrument/wmm
+goto-programs
+linking
+util
diff --git a/src/goto-programs/module_dependencies.txt b/src/goto-programs/module_dependencies.txt
new file mode 100644
index 00000000000..2b7d86a1a36
--- /dev/null
+++ b/src/goto-programs/module_dependencies.txt
@@ -0,0 +1,11 @@
+analyses # dubious - concerns call_graph and does_remove_const
+ansi-c # should go away
+assembler # should go away
+goto-programs
+goto-symex # dubious - spurious inclusion of symex_target_equation in graphml_witness
+json
+langapi # should go away
+linking
+mach-o # system
+util
+xmllang
diff --git a/src/goto-symex/module_dependencies.txt b/src/goto-symex/module_dependencies.txt
new file mode 100644
index 00000000000..047c165dd2e
--- /dev/null
+++ b/src/goto-symex/module_dependencies.txt
@@ -0,0 +1,8 @@
+analyses
+goto-programs
+goto-symex
+langapi # should go away
+linking
+pointer-analysis
+solvers
+util
diff --git a/src/jsil/module_dependencies.txt b/src/jsil/module_dependencies.txt
new file mode 100644
index 00000000000..bad90adbe0a
--- /dev/null
+++ b/src/jsil/module_dependencies.txt
@@ -0,0 +1,6 @@
+ansi-c # should go away
+goto-programs
+jsil
+langapi # should go away
+linking
+util
diff --git a/src/json/module_dependencies.txt b/src/json/module_dependencies.txt
new file mode 100644
index 00000000000..fefb43a32e6
--- /dev/null
+++ b/src/json/module_dependencies.txt
@@ -0,0 +1,2 @@
+json
+util
diff --git a/src/langapi/module_dependencies.txt b/src/langapi/module_dependencies.txt
new file mode 100644
index 00000000000..9fd7ac9f8de
--- /dev/null
+++ b/src/langapi/module_dependencies.txt
@@ -0,0 +1,3 @@
+goto-programs
+langapi
+util
diff --git a/src/linking/module_dependencies.txt b/src/linking/module_dependencies.txt
new file mode 100644
index 00000000000..e5b9de47bd8
--- /dev/null
+++ b/src/linking/module_dependencies.txt
@@ -0,0 +1,5 @@
+ansi-c # should go away
+goto-programs
+langapi # should go away
+linking
+util
diff --git a/src/memory-models/module_dependencies.txt b/src/memory-models/module_dependencies.txt
new file mode 100644
index 00000000000..f53e123b0fd
--- /dev/null
+++ b/src/memory-models/module_dependencies.txt
@@ -0,0 +1,4 @@
+cbmc # version.h
+memory-models
+langapi # should go away
+util
diff --git a/src/miniz/module_dependencies.txt b/src/miniz/module_dependencies.txt
new file mode 100644
index 00000000000..d415f87922b
--- /dev/null
+++ b/src/miniz/module_dependencies.txt
@@ -0,0 +1,2 @@
+miniz
+sys # system
diff --git a/src/nonstd/module_dependencies.txt b/src/nonstd/module_dependencies.txt
new file mode 100644
index 00000000000..55e484b8664
--- /dev/null
+++ b/src/nonstd/module_dependencies.txt
@@ -0,0 +1 @@
+nonstd
diff --git a/src/pointer-analysis/module_dependencies.txt b/src/pointer-analysis/module_dependencies.txt
new file mode 100644
index 00000000000..8962462ddc2
--- /dev/null
+++ b/src/pointer-analysis/module_dependencies.txt
@@ -0,0 +1,6 @@
+analyses
+ansi-c # should go away
+goto-programs
+langapi # should go away
+pointer-analysis
+util
diff --git a/src/solvers/cvc/module_dependencies.txt b/src/solvers/cvc/module_dependencies.txt
new file mode 100644
index 00000000000..6c95d5039c0
--- /dev/null
+++ b/src/solvers/cvc/module_dependencies.txt
@@ -0,0 +1,4 @@
+solvers/cvc
+solvers/flattening # pointer_logic.h
+solvers/prop
+util
diff --git a/src/solvers/flattening/module_dependencies.txt b/src/solvers/flattening/module_dependencies.txt
new file mode 100644
index 00000000000..275773ccac0
--- /dev/null
+++ b/src/solvers/flattening/module_dependencies.txt
@@ -0,0 +1,6 @@
+solvers/flattening
+solvers/floatbv
+solvers/lowering
+solvers/prop
+solvers/sat
+util
diff --git a/src/solvers/floatbv/module_dependencies.txt b/src/solvers/floatbv/module_dependencies.txt
new file mode 100644
index 00000000000..2f4955842ec
--- /dev/null
+++ b/src/solvers/floatbv/module_dependencies.txt
@@ -0,0 +1,3 @@
+solvers/flattening # bv_utils.h
+solvers/floatbv
+util
diff --git a/src/solvers/lowering/module_dependencies.txt b/src/solvers/lowering/module_dependencies.txt
new file mode 100644
index 00000000000..c770b3922e1
--- /dev/null
+++ b/src/solvers/lowering/module_dependencies.txt
@@ -0,0 +1,2 @@
+solvers/lowering
+util
diff --git a/src/solvers/miniBDD/module_dependencies.txt b/src/solvers/miniBDD/module_dependencies.txt
new file mode 100644
index 00000000000..555ca2e73dd
--- /dev/null
+++ b/src/solvers/miniBDD/module_dependencies.txt
@@ -0,0 +1 @@
+solvers/miniBDD
diff --git a/src/solvers/module_dependencies.txt b/src/solvers/module_dependencies.txt
new file mode 100644
index 00000000000..7ee7dcc75f2
--- /dev/null
+++ b/src/solvers/module_dependencies.txt
@@ -0,0 +1 @@
+solvers
diff --git a/src/solvers/prop/module_dependencies.txt b/src/solvers/prop/module_dependencies.txt
new file mode 100644
index 00000000000..547c16f4681
--- /dev/null
+++ b/src/solvers/prop/module_dependencies.txt
@@ -0,0 +1,3 @@
+solvers/prop
+solvers/miniBDD
+util
diff --git a/src/solvers/qbf/module_dependencies.txt b/src/solvers/qbf/module_dependencies.txt
new file mode 100644
index 00000000000..48c31e80ebe
--- /dev/null
+++ b/src/solvers/qbf/module_dependencies.txt
@@ -0,0 +1,5 @@
+quannon # external 
+solvers/prop
+solvers/qbf
+solvers/sat
+util
diff --git a/src/solvers/refinement/module_dependencies.txt b/src/solvers/refinement/module_dependencies.txt
new file mode 100644
index 00000000000..c86a2484f74
--- /dev/null
+++ b/src/solvers/refinement/module_dependencies.txt
@@ -0,0 +1,6 @@
+langapi # should go away
+solvers/flattening
+solvers/floatbv
+solvers/refinement
+solvers/sat
+util
diff --git a/src/solvers/sat/module_dependencies.txt b/src/solvers/sat/module_dependencies.txt
new file mode 100644
index 00000000000..7d087d946a3
--- /dev/null
+++ b/src/solvers/sat/module_dependencies.txt
@@ -0,0 +1,7 @@
+core # external - glucose
+simp # external - glucose
+minisat/core # external
+minisat/simp # external
+solvers/prop
+solvers/sat
+util
diff --git a/src/solvers/smt2/module_dependencies.txt b/src/solvers/smt2/module_dependencies.txt
new file mode 100644
index 00000000000..c4bd71521d1
--- /dev/null
+++ b/src/solvers/smt2/module_dependencies.txt
@@ -0,0 +1,6 @@
+solvers/flattening # boolbv_width.h and pointer_logic.h
+solvers/floatbv
+solvers/prop
+solvers/sat
+solvers/smt2
+util
diff --git a/src/util/module_dependencies.txt b/src/util/module_dependencies.txt
new file mode 100644
index 00000000000..6f311e1dcbc
--- /dev/null
+++ b/src/util/module_dependencies.txt
@@ -0,0 +1,7 @@
+big-int
+langapi # should go away
+mach # system
+malloc # system
+nonstd
+sys # system
+util
diff --git a/src/xmllang/module_dependencies.txt b/src/xmllang/module_dependencies.txt
new file mode 100644
index 00000000000..a6ec2bd6300
--- /dev/null
+++ b/src/xmllang/module_dependencies.txt
@@ -0,0 +1,2 @@
+xmllang
+util