Skip to content

Commit 612b4f8

Browse files
author
Owen Jones
committed
Address review comments
1 parent 7233f92 commit 612b4f8

5 files changed

+16
-11
lines changed

doc/architectural/background-concepts.md

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,8 @@
33

44
\author Martin Brain, Peter Schrammel
55

6+
# Representations #
7+
68
## AST: types, globals, variables, functions, code blocks, language primitives, assignments, expressions, variables ##
79

810
To be documented.
@@ -11,11 +13,13 @@ To be documented.
1113

1214
To be documented.
1315

14-
## Bounded model checking (from the CBMC manual) ##
16+
### SSA ###
1517

1618
To be documented.
1719

18-
### SSA ###
20+
# Analysis techniques #
21+
22+
## Bounded model checking (from the CBMC manual) ##
1923

2024
To be documented.
2125

doc/architectural/cprover-architecture.md renamed to doc/architectural/cbmc-architecture.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
\ingroup module_hidden
2-
\page cprover-architecture CPROVER Architecture
2+
\page cbmc-architecture CBMC Architecture
33

44
\author Martin Brain, Peter Schrammel
55

doc/architectural/compilation-and-development.md

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,6 @@
33

44
\author Martin Brain, Peter Schrammel
55

6-
# Compilation and Development
7-
86
## Makefiles ##
97

108
First off, read the \ref cbmc-user-manual "CBMC User Manual". It describes
@@ -19,10 +17,7 @@ To be documented.
1917

2018
To be documented.
2119

22-
## Generating doxygen documentation ##
23-
24-
Run `doxygen` in `/src`. HTML output will be created in `/doc/html`. The
25-
index page is `/doc/html/index.html`.
20+
## Documentation
2621

2722
Apart from the (user-orientated) CBMC user manual and this document, most
2823
of the rest of the documentation is inline in the code as `doxygen` and
@@ -31,6 +26,12 @@ contained in the `doc/` directory and gives some options for these
3126
tools. All of these could be improved and patches are very welcome. In
3227
some cases the algorithms used are described in the relevant papers.
3328

29+
## Accessing doxygen documentation ##
30+
31+
The doxygen documentation can be [accessed online](http://cprover.diffblue.com).
32+
To build it locally, run `doxygen` in `/src`. HTML output will be created in
33+
`/doc/html`. The index page is `/doc/html/index.html`.
34+
3435
## Coding standards ##
3536

3637
See <a

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,7 @@ To be documented.
8888
To be documented.
8989

9090

91-
## Examples: how to represent the AST of statements, focus on java ##
91+
## Examples: how to represent the AST of statements, in C and in java ##
9292

9393
To be documented.
9494

doc/architectural/front-page.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ you can access it <a href=
7272

7373
* \subpage background-concepts
7474

75-
* \subpage cprover-architecture
75+
* \subpage cbmc-architecture
7676

7777
* \subpage folder-walkthrough
7878

0 commit comments

Comments
 (0)