Skip to content

Commit 8b7bcb6

Browse files
author
Daniel Kroening
committed
manual: fix references
1 parent b5a998e commit 8b7bcb6

File tree

5 files changed

+6
-6
lines changed

5 files changed

+6
-6
lines changed

doc/cprover-manual/api.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@ void __CPROVER_cover(_Bool condition);
8787
```
8888
8989
This statement defines a custom coverage criterion, for usage with the
90-
[test suite generation feature](cover.shtml).
90+
[test suite generation feature](../test-suite/).
9191
9292
#### \_\_CPROVER\_isnan, \_\_CPROVER\_isfinite, \_\_CPROVER\_isinf, \_\_CPROVER\_isnormal, \_\_CPROVER\_sign
9393

doc/cprover-manual/cbmc-tutorial.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -284,7 +284,7 @@ violates an assertion. Without unwinding assertions, or when using the
284284
`--depth` command line switch, CBMC does not prove the program correct,
285285
but it can be helpful to find program bugs. The various command line
286286
options that CBMC offers for loop unwinding are described in the section
287-
on [understanding loop unwinding](../../cbmc-unwinding/).
287+
on [understanding loop unwinding](../../cbmc/unwinding/).
288288

289289
### A Note About Compilers and the ANSI-C Library
290290

doc/cprover-manual/goto-cc-variants.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
[CPROVER Manual TOC](../)
1+
[CPROVER Manual TOC](../../)
22

33
## Variants of goto-cc
44

doc/cprover-manual/goto-cc.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ The normal build system for the project may be used to build the
2020
software, but the outcome will be a model file with suitable detail for
2121
verification, as opposed to a flat executable program. Note that goto-cc
2222
comes in different variants depending on the compilation environment.
23-
These variants are described [here](goto-cc-variants.shtml).
23+
These variants are described [here](variants/).
2424

2525
### Example: Building wu-ftpd
2626

doc/cprover-manual/test-suite.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
### A Small Tutorial with a Case Study
66

77
We assume that CBMC is installed on your system. If not, follow
8-
[these instructions](../../installation/).
8+
[these instructions](../installation/).
99

1010
CBMC can be used to automatically generate test cases that satisfy a
1111
certain [code coverage](https://en.wikipedia.org/wiki/Code_coverage)
@@ -197,7 +197,7 @@ unwound enough times. For example, `climb_pid_run` needs to
197197
be called at least six times for evaluating the condition
198198
`climb_sum_err>MAX_CLIMB_SUM_ERR` in line 48 to *true*. This corresponds
199199
to Test 5. To learn more about loop unwinding take a look at [Understanding Loop
200-
Unwinding](../../cbmc-unwinding/).
200+
Unwinding](../cbmc/unwinding/).
201201

202202
In this tutorial, we present the automatic test suite generation
203203
functionality of CBMC, by applying the MC/DC code coverage criterion to

0 commit comments

Comments
 (0)