Module: ppl/ppl Branch: bounded_arithmetic Commit: 3f568dac0119fa57aea5fa923f43f80b7d0f04f9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3f568dac0119f...

Author: Roberto Bagnara bagnara@cs.unipr.it Date: Tue Apr 21 11:33:15 2009 +0200

New enumerations Bounded_Integer_Type_Width, Bounded_Integer_Type_Signedness and Bounded_Integer_Type_Overflow to encode the width, signedness and overflow behavior of bounded integer types, respectively.

---

src/globals.types.hh | 65 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 files changed, 65 insertions(+), 0 deletions(-)

diff --git a/src/globals.types.hh b/src/globals.types.hh index fe3545a..03a70bc 100644 --- a/src/globals.types.hh +++ b/src/globals.types.hh @@ -70,6 +70,71 @@ enum Optimization_Mode { MAXIMIZATION };

+//! Widths of bounded integer types. +/*! \ingroup PPL_CXX_interface */ +enum Bounded_Integer_Type_Width { + //! \hideinitializer 8 bits. + BITS_8 = 8, + + //! \hideinitializer 16 bits. + BITS_16 = 16, + + //! \hideinitializer 32 bits. + BITS_32 = 32, + + //! \hideinitializer 64 bits. + BITS_64 = 64, + + //! \hideinitializer 128 bits. + BITS_128 = 128, +}; + +//! Signedness of bounded integer types. +/*! \ingroup PPL_CXX_interface */ +enum Bounded_Integer_Type_Signedness { + //! Unsigned integer. + UNSIGNED, + + //! Signed integer represented by the two's complement of the absolute value. + SIGNED_2_COMPLEMENT +}; + +//! Overflow behavior of bounded integer types. +/*! \ingroup PPL_CXX_interface */ +enum Bounded_Integer_Type_Overflow { + /*! \brief + On overflow, wrapping takes place. + + FIXME: formally specify what "wrapping takes place" means. + */ + OVERFLOW_WRAPS, + + /*! \brief + On overflow, the result is undefined. + + This simply means that the result of the operation resulting in an + overflow can take any value. + + \note + Even though something more serious can happen in the system + being analyzed ---due to, e.g., C's undefined behavior---, here we + are only concerned with the results of arithmetic operations. + It is the responsibility of the analyzer to ensure that other + manifestations of undefined behavior are conservatively approximated. + */ + OVERFLOW_UNDEFINED, + + /*! \brief + Overflow is impossible. + + This is for the analysis of languages where overflow is trapped + before it affects the state, for which, thus, any indication that + an overflow may have affected the state is necessarily due to + the imprecision of the analysis. + */ + OVERFLOW_IMPOSSIBLE +}; + } // namespace Parma_Polyhedra_Library

#endif // !defined(PPL_globals_types_hh)