Skip to content

Minor fixes to documentation outline #2702

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Aug 10, 2018
Merged

Minor fixes to documentation outline #2702

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
adb7ef0
Minor fixes to documentation outline
Aug 9, 2018
30d29b9
Replace unicode arrows → with ascii ones ->
Aug 10, 2018
d1f2ad9
Replace -> with →
Aug 10, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions doc/architectural/background-concepts.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ##

Expand Down
12 changes: 5 additions & 7 deletions doc/architectural/cbmc-architecture.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
11 changes: 4 additions & 7 deletions doc/architectural/data-structures-core-structures-and-ast.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
22 changes: 6 additions & 16 deletions doc/architectural/data-structures-from-ast-to-goto-program.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ####

Expand All @@ -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.
16 changes: 6 additions & 10 deletions doc/architectural/front-end-languages-generating-codet-from-multiple-languages.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ###

Expand All @@ -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.