[PPL-devel] Floating-point rounding mode

[Roberto Bagnara]

Hello Tor.

On 11/10/14 03:00, Tor Myklebust wrote:
> It appears that PPL 1.1 sets the rounding mode to "upward" at startup thanks to it calling ppl_test_rounding() at startup.
> 
> Is this intentional?  It does not appear to be documented.
> 
> Will anything break if I set the rounding mode back to "nearest" at the start of main()?

The following is excerpted from the PPL 1.1 main user's manual:

void Parma Polyhedra Library::set rounding for PPL ( ) [inline]

  Sets the FPU rounding mode so that the PPL abstractions based on
  floating point numbers work correctly.  This is performed
  automatically at initialization-time. Calling this function is needed
  only if restore - pre PPL rounding() has been previously called.

void Parma Polyhedra Library::restore pre PPL rounding ( ) [inline]

  Sets the FPU rounding mode as it was before initialization of the PPL.
  This is important if the application uses floating-point computations
  outside the PPL. It is crucial when the application uses functions
  from a mathematical library that are not guaranteed to work correctly
  under all rounding modes.
  After calling this function it is absolutely necessary to call set
  rounding for PPL() before using any PPL abstractions based on floating
  point numbers. This is performed automatically at finalization-time.

Please do not hesitate to come back to us if you have further questions.
Kind regards,

   Roberto

-- 
     Prof. Roberto Bagnara

Applied Formal Methods Laboratory - University of Parma, Italy
mailto:bagnara at cs.unipr.it
                              BUGSENG srl - http://bugseng.com
                              mailto:roberto.bagnara at bugseng.com