Commit e88b2108 authored by David Bühler's avatar David Bühler
Browse files

Merge branch 'feature/dune/apron-tests' into 'master'

[eva] enable apron tests (dune)

See merge request frama-c/frama-c!3716
parents 5962c46a b6d7942c
......@@ -107,7 +107,15 @@ eva-domains:
<<: *eva_template
parallel:
matrix:
- CONFIG: ["bitwise","equality","gauges","multidim","octagon","symblocs"]
- CONFIG: [
"apron",
"bitwise",
"equality",
"gauges",
"multidim",
"octagon",
"symblocs"
]
kernel-tests:
stage: tests
......
......@@ -119,12 +119,12 @@ apron.v0.9.12 \\\
conf-graphviz.0.1 \\\
dune.3.3.1 \\\
dune-site.3.3.1 \\\
mlgmpidl.1.2.12 \\\
mlmpfr.4.1.0-bugfix2 \\\
ocamlfind.1.8.1 \\\
ocamlgraph.1.8.8 \\\
ppx_deriving_yojson.3.6.1 \\\
ppx_import.1.9.0 \\\
why3.1.5.0 \\\
why3.1.5.1 \\\
yojson.1.7.0 \\\
zarith.1.10 \\\
zmq.5.1.3 \\\
......
......@@ -4597,7 +4597,7 @@ not tainted anymore.
\label{sec:numerors}
\emph{This domain is experimental and should only be used on toy examples.\\
It requires the \texttt{mlgmpidl} library with support of MPFR,
It requires the \texttt{mlmpfr} library with support of MPFR,
provided by opam.}
\Eva{} provides a domain inferring ranges for the absolute and relative errors
......
......@@ -8,7 +8,7 @@
buildDunePackage rec {
pname = "mlmpfr";
version = "4.1.0-bugfix1";
version = "4.1.0-bugfix2";
minimumOCamlVersion = "4.04";
......@@ -16,7 +16,7 @@ buildDunePackage rec {
owner = "thvnx";
repo = pname;
rev = pname+"."+version;
sha256 = "13n6spgz5p6jhpjackvfsn33iinpadgr3v4gm63d5195mi9fgn8d";
sha256 = "19g26jv6cjinpl5pcjif1ldyaagxlandp3qjajsy8srqg4a5rg0d";
};
buildInputs = [ gmp mpfr ];
......
......@@ -33,6 +33,7 @@ let
default-config-tests = oself.callPackage ./default-config-tests.nix {};
e-acsl-tests = oself.callPackage ./e-acsl-tests.nix {};
eva-default-tests = oself.callPackage ./eva-tests.nix { config = ""; };
eva-apron-tests = oself.callPackage ./eva-tests.nix { config = "apron" ; };
eva-bitwise-tests = oself.callPackage ./eva-tests.nix { config = "bitwise" ; };
eva-equality-tests = oself.callPackage ./eva-tests.nix { config = "equality" ; };
eva-gauges-tests = oself.callPackage ./eva-tests.nix { config = "gauges" ; };
......
......@@ -38,8 +38,8 @@
"why3": {
"branch": "master",
"repo": "https://gitlab.inria.fr/why3/why3.git",
"rev": "d73deb6d1b6bc6f26936c87a0793cd666d9747e1",
"rev": "56dd530f4f63865dc88d8fcd35e2de6cc9a196d0",
"type": "git",
"version": "1.5.0"
"version": "1.5.1"
}
}
......@@ -9,6 +9,7 @@
, zarith
, menhir
, menhirLib
, mlmpfr
, js_of_ocaml
, js_of_ocaml-ppx
, ppx_deriving
......@@ -40,6 +41,7 @@ stdenv.mkDerivation rec {
zarith
menhir
menhirLib
mlmpfr
# Emacs compilation of why3.el
emacs
# Documentation
......
......@@ -120,7 +120,7 @@ depends: [
"ocaml" { >= "4.08.1" }
"ocamlfind" # needed beyond build stage, used by -load-module
"ocamlgraph" { >= "1.8.8" }
"why3" { >= "1.5.0" }
"why3" { >= "1.5.1" }
"yojson" { >= "1.6.0" & < "2.0.0" }
"zarith" { >= "1.5" }
"ppx_deriving"
......@@ -133,7 +133,7 @@ depopts: [
# libraries: because we use dynamic linking
"apron"
"coq"
"mlgmpidl"
"mlmpfr" { >= "4.1.0-bugfix2"}
"zmq"
]
......
......@@ -10,12 +10,12 @@ support libraries (notably gtksourceview). lablgtk3 should be preferred.
- apron.v0.9.13 (for eva, optional)
- coq.8.13.0 (for wp, optional)
- lablgtk3.3.1.1 + lablgtk3-sourceview3.3.1.1 | lablgtk.2.18.11
- mlgmpidl.1.2.14 (for eva, optional)
- mlmpfr.4.1.0-bugfix2 (for eva, optional)
- ocamlfind.1.8.1
- ocamlgraph.1.8.8
- ppx_deriving_yojson.3.6.1 (for mdr, optional)
- ppx_import.1.9.1
- why3.1.5.0
- why3.1.5.1
- yojson.1.7.0
- zarith.1.12
......
......@@ -23,6 +23,7 @@
open Numerors_utils
module P = Precisions
module Mpfr = Mlmpfr
(* Type declaration *)
type t = P.t * Mpfr.mpfr_float
......
......@@ -114,9 +114,7 @@ val prec : t -> Precisions.t
(** Returns the exponent of its input *)
val exponent : t -> int
(** Returns the significand of its input. This function is known to generate a
core dump if the version of your MPFR library is the 3.0.1. The version 4.0
of the library does not have the bug anymore. *)
(** Returns the significand of its input. *)
val significand : t -> t
(** Returns a element containing the same value as <dst> but with the sign
......
......@@ -84,13 +84,17 @@
(library
(name apron_domain)
(optional)
(public_name frama-c-eva.apron)
(public_name frama-c-eva.apron.core)
(flags -open Frama_c_kernel -open Eva__Private :standard -w -9)
(libraries
frama-c.kernel frama-c-eva.core
apron.octMPQ apron.boxMPQ apron.polkaMPQ apron.apron)))
;(plugin (optional) (name eva-apron) (libraries frama-c-eva.apron) (site (frama-c plugins)))
(plugin
(name eva.apron)
(optional)
(libraries frama-c-eva.apron.core)
(site (frama-c plugins)))
(rule
(targets Eva.ml Eva.mli)
......
......@@ -2,7 +2,7 @@
WP Requirements for Qualif Tests
----------------------------------------------------------
1. The Alt-Ergo theorem prover, version 2.2.0
2. The Why3 platform, version 1.5.0
2. The Why3 platform, version 1.5.1
3. The environment variable FRAMAC_WP_CACHEDIR is defined
4. The environment variable FRAMAC_WP_CACHE is defined
----------------------------------------------------------
......@@ -18,12 +18,11 @@ DEFAULT_SUITES= value/numerors value/traces
DEFAULT_SUITES= value builtins float idct
### Tests of EVA domains
apron_SUITES =
apron_SUITES = builtins float idct value
bitwise_SUITES = value builtins float idct
equality_SUITES = value builtins float idct
gauges_SUITES = value builtins float idct
multidim_SUITES = value builtins float idct
octagon_SUITES = value builtins float idct
symblocs_SUITES = value builtins float idct
# todo:
IGNORE= apron_SUITES = builtins float idct value
MACRO: EVA_MAIN_PLUGINS eva,scope
MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic
MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
MACRO: EVA_DEFAULT_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0
MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps
MACRO: RTE_TEST -rte -no-warn-invalid-pointer
......@@ -10,4 +11,4 @@ PLUGIN: @EVA_PLUGINS@
OPT: @EVA_TEST@
# Late declaration to allow redefinition of EVA_OPTIONS in subsidiary test_config files
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0
MACRO: EVA_OPTIONS @EVA_DEFAULT_OPTIONS@
MACRO: EVA_MAIN_PLUGINS eva,scope
MACRO: EVA_MAIN_PLUGINS eva,scope,eva.apron
MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic
MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
MACRO: EVA_DEFAULT_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0
MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps
MACRO: RTE_TEST -rte -no-warn-invalid-pointer
......@@ -12,4 +13,4 @@ PLUGIN: @EVA_PLUGINS@
OPT: @EVA_TEST@
# Late declaration to allow redefinition of EVA_OPTIONS in subsidiary test_config_xxx files
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains apron-octagon -eva-warn-key experimental=inactive
MACRO: EVA_OPTIONS @EVA_DEFAULT_OPTIONS@ -eva-domains apron-octagon -eva-warn-key experimental=inactive
MACRO: EVA_MAIN_PLUGINS eva,scope
MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic
MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
MACRO: EVA_DEFAULT_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0
MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps
MACRO: RTE_TEST -rte -no-warn-invalid-pointer
......@@ -12,4 +13,4 @@ PLUGIN: @EVA_PLUGINS@
OPT: @EVA_TEST@
# Late declaration to allow redefinition of EVA_OPTIONS in subsidiary test_config_xxx files
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains bitwise
MACRO: EVA_OPTIONS @EVA_DEFAULT_OPTIONS@ -eva-domains bitwise
MACRO: EVA_MAIN_PLUGINS eva,scope
MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic
MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
MACRO: EVA_DEFAULT_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0
MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps
MACRO: RTE_TEST -rte -no-warn-invalid-pointer
......@@ -12,4 +13,4 @@ PLUGIN: @EVA_PLUGINS@
OPT: @EVA_TEST@
# Late declaration to allow redefinition of EVA_OPTIONS in subsidiary test_config_xxx files
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains equality
MACRO: EVA_OPTIONS @EVA_DEFAULT_OPTIONS@ -eva-domains equality
MACRO: EVA_MAIN_PLUGINS eva,scope
MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic
MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
MACRO: EVA_DEFAULT_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0
MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps
MACRO: RTE_TEST -rte -no-warn-invalid-pointer
......@@ -12,4 +13,4 @@ PLUGIN: @EVA_PLUGINS@
OPT: @EVA_TEST@
# Late declaration to allow redefinition of EVA_OPTIONS in subsidiary test_config_xxx files
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains gauges
MACRO: EVA_OPTIONS @EVA_DEFAULT_OPTIONS@ -eva-domains gauges
MACRO: EVA_MAIN_PLUGINS eva,scope
MACRO: EVA_PLUGINS from,inout @EVA_MAIN_PLUGINS@ variadic
MACRO: EVA_CONFIG @EVA_OPTIONS@ -machdep x86_32
MACRO: EVA_DEFAULT_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0
MACRO: EVA_TEST -eva @EVA_CONFIG@ -out -input -deps
MACRO: RTE_TEST -rte -no-warn-invalid-pointer
......@@ -12,4 +13,4 @@ PLUGIN: @EVA_PLUGINS@
OPT: @EVA_TEST@
# Late declaration to allow redefinition of EVA_OPTIONS in subsidiary test_config_xxx files
MACRO: EVA_OPTIONS -eva-show-progress -eva-msg-key=-summary -eva-auto-loop-unroll 0 -eva-domains multidim -eva-warn-key experimental=inactive
MACRO: EVA_OPTIONS @EVA_DEFAULT_OPTIONS@ -eva-domains multidim -eva-warn-key experimental=inactive
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment