Fixed out of link for pages in modeling
Fixed links as follow: modeling/assumptions -> modeling-assumptions.md modeling/nondeterminism -> modeling-nondeterminism.md
This commit is contained in:
parent
1ea4a764ca
commit
bd9bfb789e
|
@ -18,7 +18,7 @@ void assert(_Bool assertion);
|
||||||
The function **\_\_CPROVER\_assume** adds an expression as a constraint
|
The function **\_\_CPROVER\_assume** adds an expression as a constraint
|
||||||
to the program. If the expression evaluates to false, the execution
|
to the program. If the expression evaluates to false, the execution
|
||||||
aborts without failure. More detail on the use of assumptions is in the
|
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
|
#### \_\_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
|
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
|
input or output values. The first argument is a string constant to
|
||||||
distinguish multiple inputs and outputs (inputs are typically generated
|
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
|
string constant is followed by an arbitrary number of values of
|
||||||
arbitrary types.
|
arbitrary types.
|
||||||
|
|
||||||
|
@ -154,7 +154,7 @@ the array **dest** with the given value.
|
||||||
|
|
||||||
#### Uninterpreted Functions
|
#### Uninterpreted Functions
|
||||||
|
|
||||||
Uninterpreted functions are documented [here](../modeling/nondeterminism/)).
|
Uninterpreted functions are documented [here](./modeling-nondeterminism.md)).
|
||||||
|
|
||||||
### Predefined Types and Symbols
|
### Predefined Types and Symbols
|
||||||
|
|
||||||
|
|
|
@ -33,7 +33,7 @@ properties together with the condition.
|
||||||
|
|
||||||
The assertion language of the CPROVER tools is identical to the language
|
The assertion language of the CPROVER tools is identical to the language
|
||||||
used for expressions. Note that
|
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
|
to check a range of choices. As an example, the following code fragment
|
||||||
asserts that **all** elements of the array are zero:
|
asserts that **all** elements of the array are zero:
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue