Add doc README.md files to each directory

Author: peterschrammel

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/README

@@ -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/ansi-c/module.md renamed to src/ansi-c/README.md

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

src/assembler/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/big-int/README

@@ -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/big-int/README.md

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

src/cbmc/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`.