Skip to content

Commit 71d62d3

Browse files
committed
Add links to CPROVER directories
Improve structure of READMEs in table of contents
1 parent 3de2445 commit 71d62d3

File tree

27 files changed

+76
-78
lines changed

27 files changed

+76
-78
lines changed

doc/architectural/cprover-architecture-overview.md

Lines changed: 24 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -56,52 +56,52 @@ rather than `UI_message_handlert` or `UIMessageHandler` and
5656

5757
- language front ends
5858

59-
* ansi-c
60-
* cpp
61-
* langapi
62-
* jsil
59+
* \ref ansi-c
60+
* \ref cpp
61+
* \ref langapi
62+
* \ref jsil
6363

6464

6565
- static analysis
6666

67-
* analysis
68-
* pointer analysis
67+
* \ref analyses
68+
* \ref pointer-analysis
6969

7070

7171
- utilities
7272

73-
* big int
74-
* json
75-
* xmllang
76-
* util
77-
* miniz
78-
* nonstd
73+
* \ref big int
74+
* \ref json
75+
* \ref xmllang
76+
* \ref util
77+
* \ref miniz
78+
* \ref nonstd
7979

8080

8181
- tools
8282

83-
* cbmc
84-
* clobber
85-
* goto-analyzer
86-
* goto-instrument
87-
* goto-diff
88-
* memory-models
89-
* goto-cc
90-
* jbmc
83+
* \ref cbmc
84+
* \ref clobber
85+
* \ref goto-analyzer
86+
* \ref goto-instrument
87+
* \ref goto-diff
88+
* \ref memory-models
89+
* \ref goto-cc
90+
* \ref jbmc
9191

9292

9393
- goto-programs
9494

95-
* goto-programs
96-
* linking
95+
* \ref goto-programs
96+
* \ref linking
9797

9898

9999
- symbolic execution
100-
* goto-symex
100+
* \ref goto-symex
101101

102102

103103
- solvers
104-
* solvers
104+
* \ref solvers
105105

106106
\section other-apps Other apps
107107
Other Useful Code

src/analyses/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
\defgroup analyses
2-
\ingroup analyses
1+
\defgroup analyses analyses
2+
# Folder analyses
33

44
FIXME: put here a good introduction describing what is contained
55
in this folder.

src/ansi-c/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
\defgroup ansi-c
2-
\ingroup ansi-c
1+
\defgroup ansi-c ansi-c
2+
# Folder ansi-c
33

44
\author Kareem Khazem
55

src/assembler/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
\defgroup assembler
2-
\ingroup assembler
1+
\defgroup assembler assembler
2+
# Folder assembler
33

44
`assembler/` is a module that serve as language front end.

src/big-int/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
\defgroup big-int
2-
\ingroup big-int
1+
\defgroup big-int big-int
2+
# Folder big-int
33

44
CPROVER is distributed with its own multi-precision arithmetic library;
55
mainly for historical and portability reasons. The library is externally

src/cbmc/README.md

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
1-
\defgroup cbmc
2-
\ingroup cbmc
3-
1+
\defgroup cbmc cbmc
2+
# Folder CBMC
43

54
The CBMC handles the code related to interacting with CBMC.

src/clobber/README.md

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
\defgroup clobber
2-
\ingroup clobber
3-
1+
\defgroup clobber clobber
2+
# Folder clobber
43
`clobber\` is a module that is a tool.

src/cpp/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
\defgroup cpp
2-
\ingroup cpp
1+
\defgroup cpp cpp
2+
# Folder cpp
33

44
The C++ Language front-end is for processing C++.

src/goto-analyzer/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
\defgroup goto-analyzer
2-
\ingroup goto-analyzer
1+
\defgroup goto-analyzer goto-analyzer
2+
# Folder goto-analyzer
33

44
`goto-analyzer/` is a module stores information related to interacting with
55
goto-analyzer. These files are medium risk to change and change frequently.

src/goto-cc/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
\defgroup goto-cc
2-
\ingroup goto-cc
1+
\defgroup goto-cc goto-cc
2+
# Folder goto-cc
33

44
`goto-cc` is a compiler replacement that just performs the first step of
55
the process; converting C or C++ programs to goto-binaries. It is

src/goto-diff/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
\defgroup goto-diff
2-
\ingroup goto-diff
1+
\defgroup goto-diff goto-diff
2+
# Folder goto-diff
33

44

55
`goto-diff/` is a module has files which change frequently and are medium

src/goto-instrument/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
\defgroup goto-instrument
2-
\ingroup goto-instrument
1+
\defgroup goto-instrument goto-instrument
2+
# Folder goto-instrument
33

44
The `goto-instrument/` directory contains a number of tools, one per
55
file, that are built into the `goto-instrument` program. All of them

src/goto-programs/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
\defgroup goto-programs
2-
\ingroup goto-programs
1+
\defgroup goto-programs goto-programs
2+
# Folder goto-programs
33

44

55
\author Kareem Khazem

src/goto-symex/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
\defgroup goto-symex
2-
\ingroup goto-symex
1+
\defgroup goto-symex goto-symex
2+
# Folder goto-symex
33

44

55
\author Kareem Khazem

src/java_bytecode/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
\defgroup java_bytecode
2-
\ingroup java_bytecode
1+
\defgroup java_bytecode java_bytecode
2+
# Folder java_bytecode
33

44

55
This module provide a front end for Java.

src/jbmc/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
\defgroup jbmc
2-
\ingroup jbmc
1+
\defgroup jbmc jbmc
2+
# Folder jbmc
33

44
`jbmc/` is like cbmc but especially designed for Java.

src/jsil/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
\defgroup jsil
2-
\ingroup jsil
1+
\defgroup jsil jsil
2+
# Folder jsil
33

44

55
`jsil/` is a module that focuses on type checking.

src/json/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
\defgroup json
2-
\ingroup json
1+
\defgroup json json
2+
# Folder json
33

44
`json/` is a utility that processes json.

src/langapi/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
\defgroup langapi
2-
\ingroup langapi
1+
\defgroup langapi langapi
2+
# Folder langapi
33

44

55
`langapi/` is a language front end.

src/linking/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
\defgroup linking
2-
\ingroup linking
1+
\defgroup linking linking
2+
# Folder linking
33

44
linking docs: todo

src/memory-models/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
\defgroup memory-models
2-
\ingroup memory-models
1+
\defgroup memory-models memory-models
2+
# Folder memory-models
33

44

55
`memory-models` is a tool that works with memory.

src/miniz/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
\defgroup miniz
2-
\ingroup miniz
1+
\defgroup miniz miniz
2+
Folder miniz
33

44

55
`miniz/` is a utility for minimizing things.

src/nonstd/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
\defgroup nonstd
2-
\ingroup nonstd
1+
\defgroup nonstd nonstd
2+
# Folder nonstd
33

44

55
`nonstd` is a utility.

src/pointer-analysis/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
\defgroup pointer-analysis
2-
\ingroup pointer-analysis
1+
\defgroup pointer-analysis pointer-analysis
2+
# Folder pointer-analysis
33

44
`pointer analysis/` is for static analysis.

src/solvers/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
\defgroup solvers
2-
\ingroup solvers
1+
\defgroup solvers solvers
2+
# Folder solvers
33

44

55
\authors Romain Brenguier, Kareem Khazem

src/util/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
\defgroup util
2-
\ingroup util
1+
\defgroup util util
2+
# Folder util
33

44

55
`util/` is filled with useful tools.

src/xmllang/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
\defgroup xmllang
2-
\ingroup xmllang
1+
\defgroup xmllang xmllang
2+
# Folder xmllang
33

44
`xmllang` is a utility for converting to XML.
55

0 commit comments

Comments
 (0)