This adds an optional dependency on MPFR to run why3execute for floats. It
is also used for reals (represented as intervals of floats).
This commit does the following changes:
- update the configure/Makefile to allow MPFR dependency
- adds a MPFR wrapper so that why3execute can still be compiled if MPFR is
not installed. In this case, an exception is raised when executing on
real/float.
- some updates are made to the standard library so that real/float
functions are part of the program world (and can be executed).
- pinterp changes to make elementary functions from real and float
executable.
- add some tests under bench/interp for manual testing of this feature
Note that the correctness of the results given for reals depends on the
precision. A too low precision may give unexpected results.
