Merge pull request #5330 from danpoe/fixes/dead-links-in-user-manual

Fix dead links in cbmc user manual

Author: danpoe

doc/cprover-manual/goto-harness.md renamed to doc/architectural/goto-harness.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
 

doc/cprover-manual/memory-analyzer.md renamed to doc/architectural/memory-analyzer.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:
 

doc/cprover-manual/restrict-function-pointer.md renamed to doc/architectural/restrict-function-pointer.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/)