From 0604d8e61b61e3a965b0390f0d654de452a5d27e Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 1 May 2020 16:51:09 +0100 Subject: [PATCH 1/2] Move documentation of more advanced features from the user manual to the developer manual --- doc/{cprover-manual => architectural}/goto-harness.md | 0 doc/{cprover-manual => architectural}/memory-analyzer.md | 0 .../restrict-function-pointer.md | 0 doc/cprover-manual/index.md | 5 +---- 4 files changed, 1 insertion(+), 4 deletions(-) rename doc/{cprover-manual => architectural}/goto-harness.md (100%) rename doc/{cprover-manual => architectural}/memory-analyzer.md (100%) rename doc/{cprover-manual => architectural}/restrict-function-pointer.md (100%) diff --git a/doc/cprover-manual/goto-harness.md b/doc/architectural/goto-harness.md similarity index 100% rename from doc/cprover-manual/goto-harness.md rename to doc/architectural/goto-harness.md diff --git a/doc/cprover-manual/memory-analyzer.md b/doc/architectural/memory-analyzer.md similarity index 100% rename from doc/cprover-manual/memory-analyzer.md rename to doc/architectural/memory-analyzer.md diff --git a/doc/cprover-manual/restrict-function-pointer.md b/doc/architectural/restrict-function-pointer.md similarity index 100% rename from doc/cprover-manual/restrict-function-pointer.md rename to doc/architectural/restrict-function-pointer.md diff --git a/doc/cprover-manual/index.md b/doc/cprover-manual/index.md index 9be7116c2a9..5ea3dd3026e 100644 --- a/doc/cprover-manual/index.md +++ b/doc/cprover-manual/index.md @@ -8,10 +8,7 @@ [A Short Tutorial](cbmc/tutorial/), [Loop Unwinding](cbmc/unwinding/), -[Assertion Checking](cbmc/assertions/), -[Restricting function pointers](cbmc/restrict-function-pointer/), -[Memory Analyzer](cbmc/memory-analyzer/), -[Program Harness](cbmc/goto-harness/) +[Assertion Checking](cbmc/assertions/) ## 4. [Test Suite Generation](test-suite/) From 93b9e97980a01b9431917c8c129e10eae420e1d7 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 1 May 2020 16:54:09 +0100 Subject: [PATCH 2/2] Fix dead links in cprover manual --- doc/cprover-manual/api.md | 2 +- doc/cprover-manual/cbmc-assertions.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/cprover-manual/api.md b/doc/cprover-manual/api.md index 85996bbbf26..e785f0cc2b1 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.md). +section on [Assumptions](../modeling/assumptions/). #### \_\_CPROVER\_r_ok, \_\_CPROVER\_w_ok diff --git a/doc/cprover-manual/cbmc-assertions.md b/doc/cprover-manual/cbmc-assertions.md index 8bbfb6ddd20..2426863ca6a 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.md) can be exploited in order +[nondeterminism](../../modeling/nondeterminism/) 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: