Add directory dependencies diagram
This commit is contained in:
parent
096decdc6c
commit
47c741c997
|
@ -82,3 +82,124 @@ develop regression tests.
|
||||||
The `unit/` directory contains the unit test suites. See
|
The `unit/` directory contains the unit test suites. See
|
||||||
\ref compilation-and-development for information on how to run and
|
\ref compilation-and-development for information on how to run and
|
||||||
develop unit tests.
|
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
|
||||||
|
|
Loading…
Reference in New Issue