From c4fba23f85614b6f560319deac2e9672729e1c29 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 16 Mar 2022 16:25:25 +0100
Subject: [PATCH] [Tests] adds tests/value
---
src/plugins/scope/dune | 2 +-
tests/ptests_config | 4 ++--
tests/value/oracle/multidim.res.oracle | 23 +++++++++++++----------
tests/value/unit_tests.ml | 2 +-
4 files changed, 17 insertions(+), 14 deletions(-)
diff --git a/src/plugins/scope/dune b/src/plugins/scope/dune
index 3c732ff0397..46f1dcdb2be 100644
--- a/src/plugins/scope/dune
+++ b/src/plugins/scope/dune
@@ -3,7 +3,7 @@
(public_name frama-c-scope.core)
(modules scope datascope zones defs)
(flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-eva.core)
+ (libraries frama-c.kernel frama-c-eva.core frama-c-inout.core)
)
(library
diff --git a/tests/ptests_config b/tests/ptests_config
index 5d3871f1993..d6197f21741 100644
--- a/tests/ptests_config
+++ b/tests/ptests_config
@@ -14,9 +14,9 @@ DEFAULT_SUITES= misc
# todo:
IGNORE= DEFAULT_SUITES= fc_script make_run_script
-DEFAULT_SUITES= value/traces
+DEFAULT_SUITES= value/traces value
# todo:
-IGNORE= DEFAULT_SUITES= test value
+IGNORE= DEFAULT_SUITES= test
# todo: adds value/numerors (requires opam package mlgmpidl and system libraries for MPFR)
IGNORE= DEFAULT_SUITES= value/numerors
diff --git a/tests/value/oracle/multidim.res.oracle b/tests/value/oracle/multidim.res.oracle
index 8c162b23ce1..771f607d995 100644
--- a/tests/value/oracle/multidim.res.oracle
+++ b/tests/value/oracle/multidim.res.oracle
@@ -26,8 +26,10 @@
# multidim: T
y1 : # cvalue: .t1[0].f ∈ {3.}
{.t1{[0].i; [1..3]}; .t2[0..3]} ∈ {0}
- # multidim: { .t1[{0}] = { .f = {3.}, .i = {0} },
- .t2[{0; 1; 2; 3}] = { .f = {0}, .i = {0} } }
+ # multidim: {
+ .t1[{0}] = { .f = {3.}.i = {0} }.t2[{0; 1; 2; 3}] = {
+ .f = {0}.i = {0}
+ } }
y2 : # cvalue: .t1[0].f ∈ {4.} or UNINITIALIZED
{.t1{[0].i; [1..3]}; .t2[0..3]} ∈ UNINITIALIZED
# multidim: { .t1[{0}] = { .f = {4.} } }
@@ -48,8 +50,10 @@
.t2[1].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
.t2[1].i ∈ [--..--]
.t2[2..3]{.f#; .i#} ∈ [0..18446744073701163007] repeated %64
- # multidim: { .t1[{0; 1; 2; 3}] = { .f = {{ ANYTHING }} },
- .t2[{0; 1; 2; 3}] = { .f = {{ ANYTHING }} } }
+ # multidim: {
+ .t1[{0; 1; 2; 3}] = { .f = {{ ANYTHING }} }.t2[{0; 1; 2; 3}] = {
+ .f = {{ ANYTHING }}
+ } }
[eva] computing for function f <- main.
Called from multidim.c:48.
[eva] using specification for function f
@@ -60,10 +64,9 @@
# multidim: [{0; 1; 2; 3}] = {
.t1[{0; 1; 2; 3}] = {
.f = [-3.40282346639e+38 .. 3.40282346639e+38]
- },
- .t2[{0; 1; 2; 3}] = {
- .f = [-3.40282346639e+38 .. 3.40282346639e+38]
- } }
+ }.t2[{0; 1; 2; 3}] = {
+ .f = [-3.40282346639e+38 .. 3.40282346639e+38]
+ } }
[eva:alarm] multidim.c:52: Warning: assertion got status unknown.
[eva] multidim.c:55: starting to merge loop iterations
[eva] multidim.c:54: starting to merge loop iterations
@@ -83,7 +86,7 @@
[3].t1[3].i ∈ {0; 2}
[3].t2[0..3] ∈ {0}
# multidim: [{0; 1; 2; 3}] = {
- .t1[{0; 1; 2; 3}] = { .f = [0. .. 2.], .i = {0; 2} } }
+ .t1[{0; 1; 2; 3}] = { .f = [0. .. 2.].i = {0; 2} } }
[eva] computing for function Frama_C_interval <- main.
Called from multidim.c:63.
[eva] using specification for function Frama_C_interval
@@ -98,7 +101,7 @@
[eva] multidim.c:65:
Frama_C_domain_show_each:
t1 : # cvalue: [--..--]
- # multidim: { .f = [0. .. 2.], .i = {0; 2} }
+ # multidim: { .f = [0. .. 2.].i = {0; 2} }
[eva] Recording results for main
[kernel] multidim.c:56: more than 0(28) elements to enumerate. Approximating.
[kernel] multidim.c:57: more than 0(28) elements to enumerate. Approximating.
diff --git a/tests/value/unit_tests.ml b/tests/value/unit_tests.ml
index 447b2e5b413..48e3b3405bc 100644
--- a/tests/value/unit_tests.ml
+++ b/tests/value/unit_tests.ml
@@ -1,3 +1,3 @@
(* Programmatic tests of Eva, run by unit_tests.i. *)
-let () = Db.Main.extend Eva.Private.Unit_tests.run
+let () = Db.Main.extend Eva.Unit_tests.run
--
GitLab