From bd9bfb789e51296ba84b5f8249518e80751ecc03 Mon Sep 17 00:00:00 2001 From: Yumi Bagge Date: Mon, 17 Jun 2019 15:37:44 +0100 Subject: [PATCH] Fixed out of link for pages in modeling Fixed links as follow: modeling/assumptions -> modeling-assumptions.md modeling/nondeterminism -> modeling-nondeterminism.md --- doc/cprover-manual/api.md | 6 +++--- doc/cprover-manual/cbmc-assertions.md | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/cprover-manual/api.md b/doc/cprover-manual/api.md index 6fce92f3ef..85996bbbf2 100644 --- a/doc/cprover-manual/api.md +++ b/doc/cprover-manual/api.md @@ -18,7 +18,7 @@ void assert(_Bool assertion); The function **\_\_CPROVER\_assume** adds an expression as a constraint to the program. If the expression evaluates to false, the execution aborts without failure. More detail on the use of assumptions is in the -section on [Assumptions](../modeling/assumptions/). +section on [Assumptions](./modeling-assumptions.md). #### \_\_CPROVER\_r_ok, \_\_CPROVER\_w_ok @@ -58,7 +58,7 @@ The functions **\_\_CPROVER\_input** and **\_\_CPROVER\_output** are used to report an input or output value. Note that they do not generate input or output values. The first argument is a string constant to distinguish multiple inputs and outputs (inputs are typically generated -using nondeterminism, as described [here](../modeling/nondeterminism/)). The +using nondeterminism, as described [here](./modeling-nondeterminism.md)). The string constant is followed by an arbitrary number of values of arbitrary types. @@ -154,7 +154,7 @@ the array **dest** with the given value. #### Uninterpreted Functions -Uninterpreted functions are documented [here](../modeling/nondeterminism/)). +Uninterpreted functions are documented [here](./modeling-nondeterminism.md)). ### Predefined Types and Symbols diff --git a/doc/cprover-manual/cbmc-assertions.md b/doc/cprover-manual/cbmc-assertions.md index 8c8c7115f2..37d75599b4 100644 --- a/doc/cprover-manual/cbmc-assertions.md +++ b/doc/cprover-manual/cbmc-assertions.md @@ -33,7 +33,7 @@ properties together with the condition. The assertion language of the CPROVER tools is identical to the language used for expressions. Note that -[nondeterminism](../../modeling-nondeterminism/) can be exploited in order +[nondeterminism](./modeling-nondeterminism.md) can be exploited in order to check a range of choices. As an example, the following code fragment asserts that **all** elements of the array are zero: