[Tests] adds tests/value

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

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

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.

tests/value/unit_tests.ml

 (* 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