@@ -23,7 +23,7 @@ The tools in the CProver project are as follows:
23
23
- [ others (converter, driver, file_converter, java-converter)] ( #others )
24
24
25
25
The rest of this document provides a section on each of these tools in alphabetical order.
26
- Most links in this document are to the [ CProver online documentation] ( http ://cprover. diffblue.com/index.html ) .
26
+ Most links in this document are to the [ CProver online documentation] ( https ://diffblue.github.io/cbmc/ ) .
27
27
28
28
29
29
## cbmc
@@ -34,39 +34,31 @@ including generating traces. This includes invoking various sub-tools and
34
34
modules.
35
35
36
36
For details on usage of the ` cbmc ` tool see the following documentation
37
- - [ Developer Tutorial] ( http ://cprover. diffblue.com /tutorial.html)
37
+ - [ Developer Tutorial] ( https ://diffblue.github.io/cbmc /tutorial.html)
38
38
includes a very brief tutorial on many aspects of ` cbmc ` and other tools.
39
39
40
40
For details on the architecture of the ` cbmc ` tool and how the analysis is performed
41
41
see the following documents:
42
- - [ CBMC Architecture] ( http ://cprover. diffblue.com /cbmc-architecture.html)
42
+ - [ CBMC Architecture] ( https ://diffblue.github.io/cbmc /cbmc-architecture.html)
43
43
gives a high level overview of the ` cbmc ` architecture and data flow.
44
- - [ Background Concepts] ( http ://cprover. diffblue.com /background-concepts.html)
44
+ - [ Background Concepts] ( https ://diffblue.github.io/cbmc /background-concepts.html)
45
45
overviews all the key concepts used in the ` cbmc ` analysis.
46
46
47
47
For details on compiling, testing, contributing, and documentation related to
48
48
development see:
49
- - [ CProver Developer Documentation] ( http ://cprover. diffblue.com/index.html )
49
+ - [ CProver Developer Documentation] ( https ://diffblue.github.io/cbmc/ )
50
50
51
51
52
52
## goto-analyzer
53
53
54
54
The ` goto-analyzer ` is a wrapper program around the
55
- [ abstract interpretation] ( http ://cprover. diffblue.com /background-concepts.html#abstract_interpretation_section)
55
+ [ abstract interpretation] ( https ://diffblue.github.io/cbmc /background-concepts.html#abstract_interpretation_section)
56
56
implementations. (For more detail on these implementations see
57
- [ here] ( http ://cprover. diffblue.com /group__analyses.html) .)
57
+ [ here] ( https ://diffblue.github.io/cbmc /group__analyses.html) .)
58
58
It is possible to configure which abstractions are used and what
59
59
is done with the chosen abstractions (verification, display,
60
- simplification, etc.). The current best documentation is available
61
- [ here] ( http://cprover.diffblue.com/goto__analyzer__parse__options_8h.html ) .
62
-
63
- Other documentation useful for this tool can be found:
64
- - [ Analysis Information] ( http://cprover.diffblue.com/group__analyses.html )
65
-
66
- Details of all the options can be seen by running
67
- ```
68
- goto-analyzer --help
69
- ```
60
+ simplification, etc.). See the [ man
61
+ page] ( https://diffblue.github.io/cbmc/man/goto-analyzer.html ) for details.
70
62
71
63
## goto-cc
72
64
@@ -81,12 +73,12 @@ will behave like `gcc`). The additional object code is used as the internal
81
73
representation for ` cbmc ` and related tools. These can also be extracted and
82
74
used themselves.
83
75
84
- Further information on ` goto-cc ` can be found:
85
- - [ Developer Tutorial] ( http ://cprover. diffblue.com /tutorial.html) with
76
+ Further information on ` goto-cc ` can be found at :
77
+ - [ Developer Tutorial] ( https ://diffblue.github.io/cbmc /tutorial.html) with
86
78
some very simple examples and notes.
87
- - [ goto-cc] ( http ://cprover. diffblue.com/group__goto -cc.html) information
79
+ - [ goto-cc] ( https ://diffblue.github.io/cbmc/man/goto -cc.html) information
88
80
on the ` goto-cc ` compilers
89
- - [ goto Programs] ( http ://cprover. diffblue.com /group__goto-programs.html)
81
+ - [ goto Programs] ( https ://diffblue.github.io/cbmc /group__goto-programs.html)
90
82
for information on goto programs and how they are used.
91
83
92
84
Note that ` goto-cc ` can emulate GCC, Visual Studio, and CodeWarrior
@@ -115,25 +107,20 @@ can then be analysed (using the harness). Harnesses can be either function
115
107
call environments, or memory snapshots.
116
108
117
109
Documentation on ` goto-harness ` can be found
118
- [ here ] ( http ://cprover. diffblue.com/md__home_travis_build_diffblue_cbmc_doc_architectural_goto -harness.html)
110
+ [ in it's man page ] ( https ://diffblue.github.io/cbmc/man/goto -harness.html)
119
111
including details and examples.
120
112
121
- Details of all the options can be seen by running
122
- ```
123
- goto-harness --help
124
- ```
125
-
126
113
127
114
## goto-instrument
128
115
129
116
This is a collection of tools for analysing and modifying goto programs
130
117
(programs created with #goto-cc). Generally these take a goto program
131
118
and output another goto program.
132
119
133
- Further examples and documentation can be found:
134
- - [ goto-instrument] ( http ://cprover. diffblue.com /group__goto-instrument.html)
120
+ Further examples and documentation can be found at :
121
+ - [ goto-instrument] ( https ://diffblue.github.io/cbmc /group__goto-instrument.html)
135
122
has an overview of ` goto-instrument ` and a small tutorial example.
136
- - [ Developer Tutorial] ( http ://cprover. diffblue.com /tutorial.html) has high
123
+ - [ Developer Tutorial] ( https ://diffblue.github.io/cbmc /tutorial.html) has high
137
124
level overview and some example commands for ` goto-instrument ` .
138
125
139
126
@@ -144,7 +131,7 @@ Java programs. This is a fork of [goto-analyzer](#goto-analyzer) with
144
131
a Java Virtual Machine front end.
145
132
146
133
Documentation useful for this tool can be found:
147
- - [ Analysis Information] ( http ://cprover. diffblue.com /group__analyses.html)
134
+ - [ Analysis Information] ( https ://diffblue.github.io/cbmc /group__analyses.html)
148
135
149
136
Details of all the options can be seen by running
150
137
```
@@ -174,13 +161,13 @@ simple examples and information.
174
161
175
162
For details on how analysis is performed in the ` cbmc ` and
176
163
` jbmc ` tools see see the following documents:
177
- - [ CBMC Architecture] ( http ://cprover. diffblue.com /cbmc-architecture.html)
164
+ - [ CBMC Architecture] ( https ://diffblue.github.io/cbmc /cbmc-architecture.html)
178
165
gives a high level overview of the ` cbmc ` architecture and data flow that * should also apply to* ` jbmc ` .
179
- - [ Background Concepts] ( http ://cprover. diffblue.com /background-concepts.html)
166
+ - [ Background Concepts] ( https ://diffblue.github.io/cbmc /background-concepts.html)
180
167
overviews all the key concepts used in the ` jbmc ` analysis.
181
168
182
169
For details on compiling, testing, contributing, and documentation related to development see:
183
- - [ CProver Development Documentation] ( http ://cprover. diffblue.com/index.html )
170
+ - [ CProver Development Documentation] ( https ://diffblue.github.io/cbmc/ )
184
171
185
172
186
173
## jdiff
@@ -212,14 +199,14 @@ Note that to use `memory-analyzer` the program must be compiled with
212
199
compile with the ` -g ` option.
213
200
214
201
For further documentation and examples see
215
- [ here] ( http ://cprover. diffblue.com/md__home_travis_build_diffblue_cbmc_doc_architectural_memory -analyzer.html) .
202
+ [ here] ( https ://diffblue.github.io/cbmc/man/memory -analyzer.html) .
216
203
217
204
218
205
## smt2_solver
219
206
220
207
This is an (Satisfiability Modulo Theories) SMT solver that
221
208
parses SMT-LIB 2 format files and uses CProver's internal bit-blasting
222
- solver (see [ solvers] ( http ://cprover. diffblue.com /group__solvers.html) )
209
+ solver (see [ solvers] ( https ://diffblue.github.io/cbmc /group__solvers.html) )
223
210
to resolve queries.
224
211
225
212
## symtab2gb
0 commit comments