Skip to content

Commit adb7ef0

Browse files
author
Owen Jones
committed
Minor fixes to documentation outline
1 parent 98657d8 commit adb7ef0

5 files changed

+23
-42
lines changed

doc/architectural/background-concepts.md

+3-3
Original file line numberDiff line numberDiff line change
@@ -13,15 +13,15 @@ To be documented.
1313

1414
To be documented.
1515

16-
### SSA ###
16+
## SSA ##
1717

1818
To be documented.
1919

2020
# Analysis techniques #
2121

22-
## Bounded model checking (from the CBMC manual) ##
22+
## Bounded model checking ##
2323

24-
To be documented.
24+
To be documented (can copy from the CBMC manual).
2525

2626
## SAT and SMT ##
2727

doc/architectural/cbmc-architecture.md

+4-6
Original file line numberDiff line numberDiff line change
@@ -59,26 +59,24 @@ transformation tools (see \ref section-other-tools).
5959

6060
To be documented.
6161

62-
## Instrumentation (for test gen & CBMC & ...): Goto functions -> goto functions ##
62+
## Instrumentation: goto functions goto functions ##
6363

6464
To be documented.
6565

66-
## Goto functions -> BMC -> Counterexample (trace) ##
66+
## Goto functions BMC Counterexample (trace) ##
6767

6868
To be documented.
6969

70-
## Trace -> interpreter -> memory map ##
70+
## Trace interpreter memory map ##
7171

7272
To be documented.
7373

74-
## Goto functions -> abstract interpretation ##
74+
## Goto functions abstract interpretation ##
7575

7676
To be documented.
7777

7878
## Executables (flow of transformations): ##
7979

80-
To be documented.
81-
8280
### goto-cc ###
8381

8482
To be documented.

doc/architectural/data-structures-core-structures-and-ast.md

+4-7
Original file line numberDiff line numberDiff line change
@@ -87,19 +87,16 @@ To be documented.
8787

8888
To be documented.
8989

90-
9190
## Examples: how to represent the AST of statements, in C and in java ##
9291

93-
To be documented.
94-
95-
### struct Array { int length, int *data }; ###
92+
### x = y + 123 ###
9693

97-
To be documented.
94+
To be documented..
9895

99-
### x = y + 123 ###
96+
### if (x > 10) { y = 2 } else { v[3] = 4 } ###
10097

10198
To be documented.
10299

103-
### if (x > 10) { y = 2 } else { v[3] = 4 } ###
100+
### Java arrays: struct Array { int length, int *data }; ###
104101

105102
To be documented.

doc/architectural/data-structures-from-ast-to-goto-program.md

+6-16
Original file line numberDiff line numberDiff line change
@@ -5,19 +5,15 @@
55

66
## goto_programt ##
77

8-
To be documented.
9-
10-
### The CFG of a function ###
11-
12-
To be documented.
8+
See \ref goto_programt.
139

1410
### instructiont ###
1511

16-
See documentation at \ref instructiont.
12+
See [instructiont](\ref goto_programt::instructiont).
1713

18-
#### Types, motivation of each type (dead?) #####
14+
#### Types, motivation of each type #####
1915

20-
To be documented.
16+
See [instructiont](\ref goto_programt::instructiont).
2117

2218
#### Accepted code (codet) values ####
2319

@@ -29,24 +25,18 @@ To be documented.
2925

3026
## goto_functionst ##
3127

32-
To be documented.
33-
34-
### A map from function names to function bodies (CFGs) ###
28+
\ref goto_functionst is a map from function names to function bodies (CFGs).
3529

3630
To be documented.
3731

3832
## goto_modelt ##
3933

40-
To be documented.
41-
42-
### A compilation unit ###
34+
\ref goto_modelt is a compilation unit.
4335

4436
To be documented.
4537

4638
## Example: ##
4739

48-
To be documented.
49-
5040
### Unsigned mult (unsigned a, unsigned b) { int acc, i; for (i = 0; i < b; i++) acc += a; return acc; } ###
5141

5242
To be documented.

doc/architectural/front-end-languages-generating-codet-from-multiple-languages.md

+6-10
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,7 @@
33

44
\author Martin Brain, Peter Schrammel
55

6-
## Front-end languages: generating codet from multiple languages ##
7-
8-
To be documented.
9-
10-
### language_uit, language_filest, languaget classes: ###
11-
12-
To be documented.
6+
## language_uit, language_filest, languaget classes: ##
137

148
### Purpose ###
159

@@ -27,14 +21,16 @@ To be documented.
2721

2822
To be documented.
2923

30-
## Java bytecode: ##
24+
## Java bytecode ##
25+
26+
### Explain how a java program / class is represented in a .class ###
3127

3228
To be documented.
3329

34-
### Explain how a java program / class is represented in a .class ###
30+
### Explain the 2 step conversion from bytecode to codet ###
3531

3632
To be documented.
3733

38-
### Explain the 2 step conversion from bytecode to codet; give an example with a class? ###
34+
### A worked example of converting java bytecode to codet ###
3935

4036
To be documented.

0 commit comments

Comments
 (0)