Add doc README.md files to each directory

src/analyses/README.md

@@ -0,0 +1,10 @@
+\ingroup module_hidden
+\defgroup analyses analyses
+
+# Folder analyses
+
+This contains the abstract interpretation framework `ai.h` and several
+static analyses that instantiate it.
+
+FIXME: put here a good introduction describing what is contained
+in this folder.

src/ansi-c/module.md → src/ansi-c/README.md

@@ -1,7 +1,27 @@
+\ingroup module_hidden
 \defgroup ansi-c ansi-c
 # Folder ansi-c
 
-\author Kareem Khazem
+\author Kareem Khazem, Martin Brain
+
+\section overview Overview
+
+Contains the front-end for ANSI C, plus a variety of common extensions.
+This parses the file, performs some basic sanity checks (this is one
+area in which the UI could be improved; patches most welcome) and then
+produces a goto-program (see below). The parser is a traditional Flex /
+Bison system.
+
+`internal_addition.c` contains the implementation of various ‘magic’
+functions that are that allow control of the analysis from the source
+code level. These include assertions, assumptions, atomic blocks, memory
+fences and rounding modes.
+
+The `library/` subdirectory contains versions of some of the C standard
+header files that make use of the CPROVER built-in functions. This
+allows CPROVER programs to be ‘aware’ of the functionality and model it
+correctly. Examples include `stdio.c`, `string.c`, `setjmp.c` and
+various threading interfaces.
 
 \section preprocessing Preprocessing & Parsing
 
@@ -24,8 +44,6 @@ digraph G {
 \enddot
 
 
-
----
 \section type-checking Type-checking
 
 In the \ref ansi-c and \ref java_bytecode directories.
@@ -112,3 +130,28 @@ called symbols. Thus, for example:
   parameter and return types of the function. The value of the symbol is
   the function's body (a \ref codet), and the symbol is stored in the
   symbol table with `foo` as the key.
+
+
+\section performance Parsing performance considerations
+
+* Measured on trunk/regression/ansi-c/windows_h_VS_2012/main.i
+
+* 13%: Copying into i_preprocessed
+
+* 5%: ansi_c_parser.read()
+
+* 53%: yyansi_clex()
+
+* 29%: parser (without typechecking)
+
+\section references Compiler References
+
+CodeWarrior C Compilers Reference 3.2:
+
+http://cache.freescale.com/files/soft_dev_tools/doc/ref_manual/CCOMPILERRM.pdf
+
+http://cache.freescale.com/files/soft_dev_tools/doc/ref_manual/ASMX86RM.pdf
+
+ARM 4.1 Compiler Reference:
+
+http://infocenter.arm.com/help/topic/com.arm.doc.dui0491c/DUI0491C_arm_compiler_reference.pdf

src/assembler/README.md

@@ -0,0 +1,6 @@
+\ingroup module_hidden
+\defgroup assembler assembler
+
+# Folder assembler
+
+`assembler/`provides front-end processing for assembler.

src/big-int/README.md

@@ -0,0 +1,14 @@
+\ingroup module_hidden
+\defgroup big-int big-int
+
+# Folder big-int
+
+\author Martin Brain
+
+CPROVER is distributed with its own multi-precision arithmetic library;
+mainly for historical and portability reasons. The library is externally
+developed and thus `big-int` contains the source as it is distributed:
+[http://www.dirk-zoller.de/](http://www.dirk-zoller.de/).
+
+This should not be used directly, see `util/mp_arith.h` for the CPROVER
+interface.

src/cbmc/README.md

@@ -0,0 +1,13 @@
+\ingroup module_hidden
+\defgroup cbmc cbmc
+
+# Folder CBMC
+
+\author Martin Brain
+
+This contains the first full application. CBMC is a bounded model
+checker that uses the front ends (`ansi-c`, `cpp`, goto-program or
+others) to create a goto-program, `goto-symex` to unwind the loops the
+given number of times and to produce and equation system and finally
+`solvers` to find a counter-example (technically, `goto-symex` is then
+used to construct the counter-example trace).

src/clobber/README.md

@@ -0,0 +1,6 @@
+\ingroup module_hidden
+\defgroup clobber clobber
+
+# Folder clobber
+
+`clobber\` is a module that is a tool.

src/cpp/README.md

@@ -0,0 +1,17 @@
+\ingroup module_hidden
+\defgroup cpp cpp
+
+# Folder cpp
+
+\author Martin Brain
+
+This directory contains the C++ front-end. It supports the subset of C++
+commonly found in embedded and system applications. Consequentially it
+doesn’t have full support for templates and many of the more advanced
+and obscure C++ features. The subset of the language that can be handled
+is being extended over time so bug reports of programs that cannot be
+parsed are useful.
+
+The functionality is very similar to the ANSI C front end; parsing the
+code and converting to goto-programs. It makes use of code from
+`langapi` and `ansi-c`.

src/goto-analyzer/README.md

@@ -0,0 +1,8 @@
+\ingroup module_hidden
+\defgroup goto-analyzer goto-analyzer
+
+# Folder goto-analyzer
+
+`goto-analyzer/` is a tool performing static analyses on goto
+programs. It provides the front end for many of the static analyses
+in the \ref analyses directory.

src/goto-cc/README.md

@@ -0,0 +1,16 @@
+\ingroup module_hidden
+\defgroup goto-cc goto-cc
+
+# Folder goto-cc
+
+\author Martin Brain
+
+`goto-cc` is a compiler replacement that just performs the first step of
+the process; converting C or C++ programs to goto-binaries. It is
+intended to be dropped in to an existing build procedure in place of the
+compiler, thus it emulates flags that would affect the semantics of the
+code produced. Which set of flags are emulated depends on the naming of
+the `goto-cc/` binary. If it is called `goto-cc` then it emulates GCC
+flags, `goto-armcc` emulates the ARM compiler, `goto-cl` emulates VCC
+and `goto-cw` emulates the Code Warrior compiler. The output of this
+tool can then be used with `cbmc` or `goto-instrument`.

src/goto-diff/README.md

@@ -0,0 +1,7 @@
+\ingroup module_hidden
+\defgroup goto-diff goto-diff
+
+# Folder goto-diff
+
+`goto-diff/` is a tool that offers functionality similar to the `diff`
+tool, but for GOTO programs.

src/goto-instrument/README.md

@@ -0,0 +1,28 @@
+\ingroup module_hidden
+\defgroup goto-instrument goto-instrument
+
+# Folder goto-instrument
+
+\author Martin Brain
+
+The `goto-instrument/` directory contains a number of tools, one per
+file, that are built into the `goto-instrument` program. All of them
+take in a goto-program (produced by `goto-cc`) and either modify it or
+perform some analysis. Examples include `nondet_static.cpp` which
+initialises static variables to a non-deterministic value,
+`nondet_volatile.cpp` which assigns a non-deterministic value to any
+volatile variable before it is read and `weak_memory.h` which performs
+the necessary transformations to reason about weak memory models. The
+exception to the “one file for each piece of functionality” rule are the
+program instrumentation options (mostly those given as “Safety checks”
+in the `goto-instrument` help text) which are included in the
+`goto-program/` directory. An example of this is
+`goto-program/stack_depth.h` and the general rule seems to be that
+transformations and instrumentation that `cbmc` uses should be in
+`goto-program/`, others should be in `goto-instrument`.
+
+`goto-instrument` is a very good template for new analysis tools. New
+developers are advised to copy the directory, remove all files apart
+from `main.*`, `parseoptions.*` and the `Makefile` and use these as the
+skeleton of their application. The `doit()` method in `parseoptions.cpp`
+is the preferred location for the top level control for the program.