diff --git a/doc/architectural/background-concepts.md b/doc/architectural/background-concepts.md index 23179891dd8..ca973284bca 100644 --- a/doc/architectural/background-concepts.md +++ b/doc/architectural/background-concepts.md @@ -13,15 +13,15 @@ To be documented. To be documented. -### SSA ### +## SSA ## To be documented. # Analysis techniques # -## Bounded model checking (from the CBMC manual) ## +## Bounded model checking ## -To be documented. +To be documented (can copy from the CBMC manual). ## SAT and SMT ## diff --git a/doc/architectural/cbmc-architecture.md b/doc/architectural/cbmc-architecture.md index eb62530b94c..38b621f3f7f 100644 --- a/doc/architectural/cbmc-architecture.md +++ b/doc/architectural/cbmc-architecture.md @@ -55,30 +55,28 @@ it’s saved output. These include a wide range of analysis and transformation tools (see \ref section-other-tools). # Concepts # -## {C, java bytecode} → Parse tree → Symbol table → GOTO programs → GOTO program transformations → BMC → counterexample (goto_tracet) → printing ## +## {C, java bytecode} → Parse tree → Symbol table → GOTO programs → GOTO program transformations → BMC → counterexample (goto_tracet) → printing ## To be documented. -## Instrumentation (for test gen & CBMC & ...): Goto functions -> goto functions ## +## Instrumentation: goto functions → goto functions ## To be documented. -## Goto functions -> BMC -> Counterexample (trace) ## +## Goto functions → BMC → Counterexample (trace) ## To be documented. -## Trace -> interpreter -> memory map ## +## Trace → interpreter → memory map ## To be documented. -## Goto functions -> abstract interpretation ## +## Goto functions → abstract interpretation ## To be documented. ## Executables (flow of transformations): ## -To be documented. - ### goto-cc ### To be documented. diff --git a/doc/architectural/data-structures-core-structures-and-ast.md b/doc/architectural/data-structures-core-structures-and-ast.md index 84a3646e7e0..4b0c1b1a3a8 100644 --- a/doc/architectural/data-structures-core-structures-and-ast.md +++ b/doc/architectural/data-structures-core-structures-and-ast.md @@ -87,19 +87,16 @@ To be documented. To be documented. - ## Examples: how to represent the AST of statements, in C and in java ## -To be documented. - -### struct Array { int length, int *data }; ### +### x = y + 123 ### -To be documented. +To be documented.. -### x = y + 123 ### +### if (x > 10) { y = 2 } else { v[3] = 4 } ### To be documented. -### if (x > 10) { y = 2 } else { v[3] = 4 } ### +### Java arrays: struct Array { int length, int *data }; ### To be documented. diff --git a/doc/architectural/data-structures-from-ast-to-goto-program.md b/doc/architectural/data-structures-from-ast-to-goto-program.md index 1429a397f98..b16394a72a5 100644 --- a/doc/architectural/data-structures-from-ast-to-goto-program.md +++ b/doc/architectural/data-structures-from-ast-to-goto-program.md @@ -5,19 +5,15 @@ ## goto_programt ## -To be documented. - -### The CFG of a function ### - -To be documented. +See \ref goto_programt. ### instructiont ### -See documentation at \ref instructiont. +See [instructiont](\ref goto_programt::instructiont). -#### Types, motivation of each type (dead?) ##### +#### Types, motivation of each type ##### -To be documented. +See [instructiont](\ref goto_programt::instructiont). #### Accepted code (codet) values #### @@ -29,24 +25,18 @@ To be documented. ## goto_functionst ## -To be documented. - -### A map from function names to function bodies (CFGs) ### +\ref goto_functionst is a map from function names to function bodies (CFGs). To be documented. ## goto_modelt ## -To be documented. - -### A compilation unit ### +\ref goto_modelt is a compilation unit. To be documented. ## Example: ## -To be documented. - ### Unsigned mult (unsigned a, unsigned b) { int acc, i; for (i = 0; i < b; i++) acc += a; return acc; } ### To be documented. diff --git a/doc/architectural/front-end-languages-generating-codet-from-multiple-languages.md b/doc/architectural/front-end-languages-generating-codet-from-multiple-languages.md index 6b8c6b82d53..3519239cfea 100644 --- a/doc/architectural/front-end-languages-generating-codet-from-multiple-languages.md +++ b/doc/architectural/front-end-languages-generating-codet-from-multiple-languages.md @@ -3,13 +3,7 @@ \author Martin Brain, Peter Schrammel -## Front-end languages: generating codet from multiple languages ## - -To be documented. - -### language_uit, language_filest, languaget classes: ### - -To be documented. +## language_uit, language_filest, languaget classes: ## ### Purpose ### @@ -27,14 +21,16 @@ To be documented. To be documented. -## Java bytecode: ## +## Java bytecode ## + +### Explain how a java program / class is represented in a .class ### To be documented. -### Explain how a java program / class is represented in a .class ### +### Explain the 2 step conversion from bytecode to codet ### To be documented. -### Explain the 2 step conversion from bytecode to codet; give an example with a class? ### +### A worked example of converting java bytecode to codet ### To be documented.