From adb7ef05aeafd321dcc82f81277dbace5ee6a55c Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Thu, 9 Aug 2018 16:45:08 +0100 Subject: [PATCH 1/3] Minor fixes to documentation outline --- doc/architectural/background-concepts.md | 6 ++--- doc/architectural/cbmc-architecture.md | 10 ++++----- ...data-structures-core-structures-and-ast.md | 11 ++++------ ...ata-structures-from-ast-to-goto-program.md | 22 +++++-------------- ...enerating-codet-from-multiple-languages.md | 16 +++++--------- 5 files changed, 23 insertions(+), 42 deletions(-) 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..933865afc17 100644 --- a/doc/architectural/cbmc-architecture.md +++ b/doc/architectural/cbmc-architecture.md @@ -59,26 +59,24 @@ transformation tools (see \ref section-other-tools). 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. From 30d29b92558df33ed9adfe1fcdb07e19794ff1b3 Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Fri, 10 Aug 2018 10:58:17 +0100 Subject: [PATCH 2/3] =?UTF-8?q?Replace=20unicode=20arrows=20=E2=86=92=20wi?= =?UTF-8?q?th=20ascii=20ones=20->?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- doc/architectural/cbmc-architecture.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/doc/architectural/cbmc-architecture.md b/doc/architectural/cbmc-architecture.md index 933865afc17..354fca78309 100644 --- a/doc/architectural/cbmc-architecture.md +++ b/doc/architectural/cbmc-architecture.md @@ -55,23 +55,23 @@ 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: 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. From d1f2ad9762d6cac27a6274fef8f8429d629d60d2 Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Fri, 10 Aug 2018 11:53:30 +0100 Subject: [PATCH 3/3] Replace -> with → --- doc/architectural/cbmc-architecture.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/doc/architectural/cbmc-architecture.md b/doc/architectural/cbmc-architecture.md index 354fca78309..38b621f3f7f 100644 --- a/doc/architectural/cbmc-architecture.md +++ b/doc/architectural/cbmc-architecture.md @@ -55,23 +55,23 @@ 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: 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.