[PPL-devel] [GIT] ppl/ppl(master): Added more in the section about the wrapping operator.

[Roberto Bagnara]

Module: ppl/ppl
Branch: master
Commit: c3dd71f3d2a0c91b1bb493757c9bcaf7d3e2e3c4
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c3dd71f3d2a0c91b1bb493757c9bcaf7d3e2e3c4

Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date:   Sun May 17 08:44:42 2009 +0200

Added more in the section about the wrapping operator.

---

 doc/definitions.dox |   11 +++++++++++
 1 files changed, 11 insertions(+), 0 deletions(-)

diff --git a/doc/definitions.dox b/doc/definitions.dox
index c11b9cc..c651cdf 100644
--- a/doc/definitions.dox
+++ b/doc/definitions.dox
@@ -512,6 +512,17 @@ tracking multiple program variables.  Secondly, the integers modulo
 and multiplication are well defined.  This means, e.g., that assignments
 with affine right-hand sides and involving only variables with the same
 bit-width and representation can be safely modeled by affine images.
+While upper bounds and widening can be used without any precaution,
+anything that can be reconducted to intersection requires a preliminary
+<EM>wrapping</EM> phase, where the dimensions corresponding to bounded
+integer types are brought back to their natural domain.
+This necessity arise naturally for the analysis of conditionals
+and conversion operators, as well as in the realization of domain
+combinations.
+
+The PPL provides a general wrapping operator that is parametric with
+respect to the set of space dimensions (variables) to be wrapped,
+the width, representation and overflow behavior of all these variables,
 
 FIXME(0.11): to be continued.