Improve code contract documentation

[feliperodri]

CBMC version: > 5.12
Operating system: N/A.
Exact command line resulting in the issue: N/A.
What behaviour did you expect: Complete documentation for current code contract support.
What happened instead:

Currently, CPROVER Manual doesn't have a complete documentation for code contracts (e.g., __CPROVER_ensures, __CPROVER_requires, __CPROVER_assigns, etc.). There should be a section in the manual describing the current support for these features. Particularly, improve the current section for assigns clauses:

1. The documentation of assigns clause should clarify how CBMC checks that memory not captured by an assigns clause will not be written within a given scope;
2. Improve explanation in Semantic. Enforcement subsection on how an assigns clause is a sound characterization
   of the behavior of a given function.

[feliperodri]

#6185 solves this issue.