diff --git a/doc/architectural/folder-walkthrough.md b/doc/architectural/folder-walkthrough.md index 59e0b2aa43e..0ae4eab3fc7 100644 --- a/doc/architectural/folder-walkthrough.md +++ b/doc/architectural/folder-walkthrough.md @@ -35,11 +35,9 @@ containing the code for a different part of the system. - Tools * \ref cbmc - * \ref clobber * \ref goto-analyzer * \ref goto-instrument * \ref goto-diff - * \ref memory-models * \ref goto-cc * \ref jbmc @@ -84,3 +82,124 @@ develop regression tests. The `unit/` directory contains the unit test suites. See \ref compilation-and-development for information on how to run and develop unit tests. + +## Directory dependencies ## + +This diagram shows *intended* directory dependencies. Arrows should +be read transitively - dependencies of dependencies are often used +directly. + +There are `module_dependencies.txt` files in each directory, +which are checked by the linter. Where directories in `module_dependencies.txt` +are marked with comments such as 'dubious' or 'should go away', these +dependencies have generally not been included in the diagram. + +\dot +digraph directory_dependencies { + node [style = filled, color = white]; + + subgraph cluster_executables { + label = "Executables"; + style = filled; + color = lightgrey; + node [style = filled, color = white]; + CBMC [URL = "\ref cbmc"]; + goto_cc [label = "goto-cc", URL = "\ref goto-cc"]; + goto_analyzer [label = "goto-analyzer", URL = "\ref goto-analyzer"]; + goto_instrument [label = "goto-instrument", URL = "\ref goto-instrument"]; + goto_diff [label = "goto-diff", URL = "\ref goto-diff"]; + janalyzer [URL = "\ref janalyzer"]; + jdiff [URL = "\ref jdiff"]; + JBMC [URL = "\ref jbmc"]; + smt2_solver; + } + + subgraph cluster_symbolic_execution { + label = "Symbolic Execution"; + style = filled; + color = lightgrey; + node [style = filled, color = white]; + goto_symex [label = "goto-symex", URL = "\ref goto-symex"]; + } + + subgraph cluster_abstract_interpretation { + label = "Abstract Interpretation"; + style = filled; + color = lightgrey; + node [style = filled, color = white]; + pointer_analysis [label = "pointer-analysis", URL = "\ref pointer-analysis"]; + analyses [URL = "\ref analyses"]; + } + + subgraph cluster_goto_programs { + label = "Goto Programs"; + style = filled; + color = lightgrey; + goto_programs [label = "goto-programs", URL = "\ref goto-programs"]; + linking [URL = "\ref linking"]; + } + + subgraph cluster_solvers { + label = "Solvers" + style = filled; + color = lightgrey; + solvers [URL = "\ref solvers"]; + } + + subgraph cluster_languages { + label = "Languages"; + style = filled; + color = lightgrey; + ansi_c [label = "ansi-c", URL = "\ref ansi-c"]; + langapi [URL = "\ref langapi"]; + cpp [URL = "\ref cpp"]; + jsil [URL = "\ref jsil"]; + java_bytecode [URL = "\ref java_bytecode"]; + } + + subgraph cluster_utilities { + label = "Utilities"; + style = filled; + color = lightgrey; + big_int [label = "big-int", URL = "\ref big-int"]; + miniz [URL = "\ref miniz"]; + util [URL = "\ref util"]; + nonstd [URL = "\ref nonstd"]; + json [URL = "\ref json"]; + xmllang [URL = "\ref xmllang"]; + assembler [URL = "\ref assembler"]; + } + + JBMC -> { CBMC, java_bytecode }; + jdiff -> { goto_diff, java_bytecode }; + janalyzer -> { goto_analyzer, java_bytecode }; + CBMC -> { goto_instrument, jsil }; + goto_diff -> { goto_instrument }; + goto_analyzer -> { analyses, jsil, cpp }; + goto_instrument -> { goto_symex, cpp }; + goto_cc -> { cpp, jsil }; + smt2_solver -> solvers; + + java_bytecode -> { analyses, miniz }; + jsil -> linking; + cpp -> ansi_c; + ansi_c -> langapi; + langapi -> goto_programs; + + goto_symex -> { solvers, pointer_analysis }; + + pointer_analysis -> { analyses, goto_programs }; + analyses -> pointer_analysis; + + solvers -> util; + + linking -> goto_programs; + goto_programs -> { linking, xmllang, json, assembler }; + + json -> util; + xmllang -> util; + assembler -> util; + util -> big_int; + util -> nonstd; +} +\enddot