• Sylvain Dailler's avatar
    why3execute: Add execution for floats and reals (depends from mpfr) · ae5ddf91
    Sylvain Dailler authored
    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.
    ae5ddf91
Name
Last commit
Last update
bench Loading commit data...
doc Loading commit data...
drivers Loading commit data...
examples Loading commit data...
lib Loading commit data...
misc Loading commit data...
opam Loading commit data...
plugins Loading commit data...
share Loading commit data...
src Loading commit data...
stdlib Loading commit data...
tests Loading commit data...
.dockerignore Loading commit data...
.gitattributes Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
.mailmap Loading commit data...
.merlin.in Loading commit data...
.ocp-indent Loading commit data...
AUTHORS Loading commit data...
CHANGES.md Loading commit data...
DEVELOPER.readme Loading commit data...
INSTALL.md Loading commit data...
LICENSE Loading commit data...
Makefile.in Loading commit data...
OCAML-LICENSE Loading commit data...
README.md Loading commit data...
ROADMAP Loading commit data...
TODO Loading commit data...
Version Loading commit data...
autogen.sh Loading commit data...
check.sh Loading commit data...
configure.in Loading commit data...