From b6e1c3bfa9ff1cb7814fc9aa7de9d33fa9ad10ca Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 30 Sep 2020 23:00:12 +0200
Subject: [PATCH] Tests add journal directory
---
Makefile | 2 +-
ptests/ptests.ml | 5 ++-
src/plugins/value/Eva.mli | 52 ++++++++++++-----------
tests/journal/control.i | 8 ++--
tests/journal/control2.c | 9 ++--
tests/journal/intra.i | 4 +-
tests/journal/oracle/control.0.res.oracle | 3 +-
tests/journal/oracle/control.1.res.oracle | 6 +--
tests/journal/oracle/control2.res.oracle | 10 ++---
tests/journal/oracle/control2_sav.res | 12 +++---
tests/journal/oracle/intra.res.oracle | 32 +++++++-------
11 files changed, 73 insertions(+), 70 deletions(-)
diff --git a/Makefile b/Makefile
index 229bb16d7d4..2480471e21d 100644
--- a/Makefile
+++ b/Makefile
@@ -168,7 +168,7 @@ force-reconfigure:
##############################################################################
.PHONY: tests clean-tests
-TESTS=builtins callgraph cil constant_propagation float idct impact libc metrics misc occurrence pdg rte rte_manual scope slicing sparecode syntax test value jcdb
+TESTS=builtins callgraph cil constant_propagation float idct impact libc metrics misc occurrence pdg rte rte_manual scope slicing sparecode syntax test value jcdb journal
tests: config.sed
find tests -name dune | grep -e "oracle.*/\|result.*/" | xargs --no-run-if-empty rm
dune exec -- ptests/ptests.exe
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 0a8c10a46d3..824dce6ed06 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -1061,6 +1061,7 @@ module Fmt = struct
let quote pr fmt s = Format.fprintf fmt "%S" (Format.asprintf "%a" pr s)
let list pr fmt l = List.iter (fun s -> Format.fprintf fmt " %a" pr s) l
let var_libavailable pr fmt s = Format.fprintf fmt "%%{lib-available:%a}" pr s
+ let package_as_deps pr fmt s = Format.fprintf fmt "(package %a)" pr s
end
let command_string ~result_fmt ~oracle_fmt command =
@@ -1137,7 +1138,6 @@ let command_string ~result_fmt ~oracle_fmt command =
* in *)
let macros = get_macros command in
let deps = List.map (Macros.expand macros) command.deps in
- let package_as_deps pr fmt s = Format.fprintf fmt "(package %a)" pr s in
Format.fprintf result_fmt
"(rule\n \
(targets %S %S %a)\n \
@@ -1717,10 +1717,13 @@ let dispatcher ~result_fmt ~oracle_fmt file directory config =
Format.fprintf result_fmt "\
(rule
(alias ptests)
+ (deps %a (package frama-c)%a)
(targets %a %a)
(action (system %S))
)
"
+ print_list config.dc_deps
+ Fmt.(list (package_as_deps (quote plugin_as_package))) config.dc_plugins
print_list res.ex_log
print_list res.ex_bin
res.ex_cmd
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 096db791027..12777dde807 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -22,6 +22,33 @@
(** Analysis for values and pointers *)
+
+(** For internal use *)
+
+module Private: sig
+ module Abstractions = Abstractions
+ module Analysis = Analysis
+ module Alarmset = Alarmset
+ module Main_values = Main_values
+ module Value_parameters =Value_parameters
+ module Eval = Eval
+ module Eval_terms = Eval_terms
+ module Red_statuses = Red_statuses
+ module Abstract_value = Abstract_value
+ module Abstract_domain = Abstract_domain
+ module Mark_noresults = Mark_noresults
+ module Simple_memory = Simple_memory
+ module Structure = Structure
+ module Eval_typ = Eval_typ
+ module Eval_op = Eval_op
+ module Value_util = Value_util
+ module Value_results = Value_results
+ module Domain_builder = Domain_builder
+ module Main_locations = Main_locations
+ module Eval_annots = Eval_annots
+end
+
+
module Value_results: sig
type results
@@ -97,28 +124,3 @@ module Eva_annotations: sig
val add_subdivision_annot : emitter:Emitter.t -> loc:Cil_types.location ->
Cil_types.stmt -> int -> unit
end
-
-(** For internal use *)
-
-module Private: sig
- module Abstractions = Eva__Abstractions
- module Analysis = Eva__Analysis
- module Alarmset = Eva__Alarmset
- module Main_values = Eva__Main_values
- module Value_parameters =Eva__Value_parameters
- module Eval = Eva__Eval
- module Eval_terms = Eva__Eval_terms
- module Red_statuses = Eva__Red_statuses
- module Abstract_value = Eva__Abstract_value
- module Abstract_domain = Eva__Abstract_domain
- module Mark_noresults = Eva__Mark_noresults
- module Simple_memory = Eva__Simple_memory
- module Structure = Eva__Structure
- module Eval_typ = Eva__Eval_typ
- module Eval_op = Eva__Eval_op
- module Value_util = Eva__Value_util
- module Value_results = Eva__Value_results
- module Domain_builder = Eva__Domain_builder
- module Main_locations = Eva__Main_locations
- module Eval_annots = Eva__Eval_annots
-end
diff --git a/tests/journal/control.i b/tests/journal/control.i
index 9a666496980..7611474cf1e 100644
--- a/tests/journal/control.i
+++ b/tests/journal/control.i
@@ -1,12 +1,12 @@
/* run.config
COMMENT: do not compare generated journals since they depend on current time
- EXECNOW: BIN control_journal.ml BIN control_journal_bis.ml (frama-c -journal-enable -check -eva -deps -out @EVA_OPTIONS@ -main f -journal-name control_journal.ml control.i && cp control_journal.ml control_journal_bis.ml) > /dev/null 2> /dev/null
+ EXECNOW: BIN control_journal.ml BIN control_journal_bis.ml (frama-c -journal-enable -check -eva -deps -out @EVA_CONFIG@ -main f -journal-name control_journal.ml control.i && cp control_journal.ml control_journal_bis.ml) > /dev/null 2> /dev/null
CMD: frama-c
- OPT: -load-script control_journal -journal-disable
+ OPT: -load-script %{dep:control_journal.ml} -journal-disable
CMD: frama-c
- OPT: -load-script control_journal_bis -calldeps -journal-disable
+ OPT: -load-script %{dep:control_journal_bis.ml} -calldeps -journal-disable
CMXS: abstract_cpt
- EXECNOW: BIN abstract_cpt_journal.ml frama-c -journal-enable -load-module abstract_cpt -load-script %{dep:use_cpt.ml} -journal-name abstract_cpt_journal.ml > /dev/null 2> /dev/null
+ EXECNOW: BIN abstract_cpt_journal.ml frama-c -journal-enable -load-module %{dep:abstract_cpt.cmxs} -load-script %{dep:use_cpt.ml} -journal-name abstract_cpt_journal.ml > /dev/null 2> /dev/null
CMD: frama-c
OPT: -load-script %{dep:abstract_cpt_journal.ml} -load-module abstract_cpt -load-script %{dep:use_cpt.ml}
*/
diff --git a/tests/journal/control2.c b/tests/journal/control2.c
index 8b8d36c5130..1f948050fe0 100644
--- a/tests/journal/control2.c
+++ b/tests/journal/control2.c
@@ -1,8 +1,9 @@
/* run.config
- EXECNOW: BIN control_journal2.ml ./bin/toplevel.opt -journal-enable -eva -deps -out -main f -journal-name result/control_journal2.ml control2.c > /dev/null 2> /dev/null
- EXECNOW: LOG control2_sav.res LOG control2_sav.err BIN control_journal_next2.ml FRAMAC_LIB=lib/fc ./bin/toplevel.byte -journal-enable -load-script %{dep:control_journal2} -lib-entry -journal-name control_journal_next2.ml control2.c > ./result/control2_sav.res 2> ./result/control2_sav.err
- CMD: FRAMAC_LIB=lib/fc ./bin/toplevel.byte
- OPT: -load-script result/control_journal_next2
+ PLUGIN: callgraph
+ EXECNOW: BIN control_journal2.ml PTESTS_ITS_NOT_FRAMAC=yes frama-c -no-autoload-plugins -load-plugin from,inout,eva,scope,variadic -journal-enable -eva -deps -out -main f -journal-name control_journal2.ml control2.c > /dev/null 2> /dev/null
+ EXECNOW: LOG control2_sav.res LOG control2_sav.err BIN control_journal_next2.ml PTESTS_ITS_NOT_FRAMAC=yes frama-c -no-autoload-plugins -load-plugin from,inout,eva,scope,variadic -journal-enable -load-script %{dep:control_journal2.ml} -lib-entry -journal-name control_journal_next2.ml control2.c > control2_sav.res 2> control2_sav.err
+ CMD: PTESTS_ITS_NOT_FRAMAC=yes frama-c
+ OPT: -load-script %{dep:control_journal_next2.ml}
*/
int x,y,c,d;
diff --git a/tests/journal/intra.i b/tests/journal/intra.i
index 268a1ad8530..cadfe3ac742 100644
--- a/tests/journal/intra.i
+++ b/tests/journal/intra.i
@@ -1,9 +1,9 @@
/* run.config
PLUGIN: sparecode
CMXS: @PTEST_NAME@
- EXECNOW: BIN intra_journal.ml @frama-c@ -eva-show-progress -load-module %{dep:@PTEST_NAME@.cmxs} -journal-enable -journal-name result/intra_journal.ml @PTEST_DIR@/@PTEST_NAME@.i > /dev/null 2> /dev/null
+ EXECNOW: BIN intra_journal.ml PTESTS_IT_IS_NOT_FRAMAC=yes @frama-c@ -eva-show-progress -no-autoload-plugins -load-plugin from,inout,eva,scope,variadic,sparecode -load-module %{dep:@PTEST_NAME@.cmxs} -journal-enable -journal-name intra_journal.ml @PTEST_NAME@.i > /dev/null 2> /dev/null
CMD: @frama-c@ -load-module %{dep:@PTEST_NAME@.cmxs}
- OPT: -load-script result/intra_journal -journal-disable
+ OPT: -load-script %{dep:intra_journal.ml} -journal-disable
*/
/* Waiting for results such as:
diff --git a/tests/journal/oracle/control.0.res.oracle b/tests/journal/oracle/control.0.res.oracle
index c03380ec1e4..cde4638dac2 100644
--- a/tests/journal/oracle/control.0.res.oracle
+++ b/tests/journal/oracle/control.0.res.oracle
@@ -8,8 +8,7 @@
c ∈ {0}
d ∈ {0}
[eva] control.i:18: starting to merge loop iterations
-[eva:alarm] control.i:21: Warning:
- signed overflow. assert x + 1 ≤ 2147483647;
+[eva:alarm] control.i:21: Warning: signed overflow. assert x + 1 ≤ 2147483647;
[eva] Recording results for f
[eva] done for function f
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/journal/oracle/control.1.res.oracle b/tests/journal/oracle/control.1.res.oracle
index ee218e0dec6..bcba463677d 100644
--- a/tests/journal/oracle/control.1.res.oracle
+++ b/tests/journal/oracle/control.1.res.oracle
@@ -8,8 +8,7 @@
c ∈ {0}
d ∈ {0}
[eva] control.i:18: starting to merge loop iterations
-[eva:alarm] control.i:21: Warning:
- signed overflow. assert x + 1 ≤ 2147483647;
+[eva:alarm] control.i:21: Warning: signed overflow. assert x + 1 ≤ 2147483647;
[eva] Recording results for f
[eva] done for function f
[eva] ====== VALUES COMPUTED ======
@@ -44,8 +43,7 @@
y ∈ {0}
c ∈ {0}
d ∈ {0}
-[eva:alarm] control.i:21: Warning:
- signed overflow. assert x + 1 ≤ 2147483647;
+[eva:alarm] control.i:21: Warning: signed overflow. assert x + 1 ≤ 2147483647;
[eva] Recording results for f
[from] Computing for function f
[from] Done for function f
diff --git a/tests/journal/oracle/control2.res.oracle b/tests/journal/oracle/control2.res.oracle
index acf4746fb0c..92d19a0804c 100644
--- a/tests/journal/oracle/control2.res.oracle
+++ b/tests/journal/oracle/control2.res.oracle
@@ -7,8 +7,8 @@
y ∈ {0}
c ∈ {0}
d ∈ {0}
-[eva] control2.c:12: starting to merge loop iterations
-[eva:alarm] control2.c:15: Warning:
+[eva] control2.c:13: starting to merge loop iterations
+[eva:alarm] control2.c:16: Warning:
signed overflow. assert x + 1 ≤ 2147483647;
[eva] done for function f
[eva] ====== VALUES COMPUTED ======
@@ -37,11 +37,11 @@
y ∈ [--..--]
c ∈ [--..--]
d ∈ [--..--]
-[eva:alarm] control2.c:13: Warning:
+[eva:alarm] control2.c:14: Warning:
signed overflow. assert y + 1 ≤ 2147483647;
-[eva:alarm] control2.c:13: Warning:
+[eva:alarm] control2.c:14: Warning:
signed overflow. assert x + 1 ≤ 2147483647;
-[eva:alarm] control2.c:15: Warning:
+[eva:alarm] control2.c:16: Warning:
signed overflow. assert x + 1 ≤ 2147483647;
[eva] done for function f
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/journal/oracle/control2_sav.res b/tests/journal/oracle/control2_sav.res
index 3fb8ddd2c4f..fbebf504547 100644
--- a/tests/journal/oracle/control2_sav.res
+++ b/tests/journal/oracle/control2_sav.res
@@ -7,8 +7,8 @@
y ∈ {0}
c ∈ {0}
d ∈ {0}
-[eva] control2.c:12: starting to merge loop iterations
-[eva:alarm] control2.c:15: Warning:
+[eva] control2.c:13: starting to merge loop iterations
+[eva:alarm] control2.c:16: Warning:
signed overflow. assert x + 1 ≤ 2147483647;
[eva] done for function f
[eva] ====== VALUES COMPUTED ======
@@ -38,11 +38,11 @@
y ∈ [--..--]
c ∈ [--..--]
d ∈ [--..--]
-[eva:alarm] control2.c:13: Warning:
+[eva:alarm] control2.c:14: Warning:
signed overflow. assert y + 1 ≤ 2147483647;
-[eva:alarm] control2.c:13: Warning:
+[eva:alarm] control2.c:14: Warning:
signed overflow. assert x + 1 ≤ 2147483647;
-[eva:alarm] control2.c:15: Warning:
+[eva:alarm] control2.c:16: Warning:
signed overflow. assert x + 1 ≤ 2147483647;
[eva] done for function f
[eva] ====== VALUES COMPUTED ======
@@ -74,4 +74,4 @@
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function f:
x; y; i
-[kernel] writing journal in file `result/control_journal_next2.ml'.
+[kernel] writing journal in file `control_journal_next2.ml'.
diff --git a/tests/journal/oracle/intra.res.oracle b/tests/journal/oracle/intra.res.oracle
index 1d0c56f4f1d..5c5c77181c9 100644
--- a/tests/journal/oracle/intra.res.oracle
+++ b/tests/journal/oracle/intra.res.oracle
@@ -8,49 +8,49 @@
X10 ∈ {0}
Y10 ∈ {0}
[eva] computing for function param <- main.
- Called from intra.i:81.
+ Called from intra.i:82.
[eva] Recording results for param
[eva] Done for function param
[eva] computing for function tmp <- main.
- Called from intra.i:82.
-[eva] intra.i:20: assertion got status valid.
-[eva] intra.i:22: assertion got status valid.
+ Called from intra.i:83.
+[eva] intra.i:21: assertion got status valid.
+[eva] intra.i:23: assertion got status valid.
[eva] Recording results for tmp
[eva] Done for function tmp
[eva] computing for function spare_called_fct <- main.
- Called from intra.i:83.
+ Called from intra.i:84.
[eva] Recording results for spare_called_fct
[eva] Done for function spare_called_fct
[eva] computing for function call_two_outputs <- main.
- Called from intra.i:84.
+ Called from intra.i:85.
[eva] computing for function two_outputs <- call_two_outputs <- main.
- Called from intra.i:48.
+ Called from intra.i:49.
[eva] Recording results for two_outputs
[eva] Done for function two_outputs
[eva] computing for function two_outputs <- call_two_outputs <- main.
- Called from intra.i:52.
+ Called from intra.i:53.
[eva] Recording results for two_outputs
[eva] Done for function two_outputs
[eva] Recording results for call_two_outputs
[eva] Done for function call_two_outputs
[eva] computing for function loop <- main.
- Called from intra.i:85.
-[eva] intra.i:63: assertion got status valid.
-[eva] intra.i:64: loop invariant got status valid.
-[eva] intra.i:66: starting to merge loop iterations
+ Called from intra.i:86.
+[eva] intra.i:64: assertion got status valid.
+[eva] intra.i:65: loop invariant got status valid.
+[eva] intra.i:67: starting to merge loop iterations
[eva] Recording results for loop
[eva] Done for function loop
[eva] computing for function assign <- main.
- Called from intra.i:86.
+ Called from intra.i:87.
[eva] Recording results for assign
[eva] Done for function assign
[eva] computing for function assign <- main.
- Called from intra.i:87.
+ Called from intra.i:88.
[eva] Recording results for assign
[eva] Done for function assign
[eva] computing for function stop <- main.
- Called from intra.i:90.
-[kernel:annot:missing-spec] intra.i:90: Warning:
+ Called from intra.i:91.
+[kernel:annot:missing-spec] intra.i:91: Warning:
Neither code nor specification for function stop, generating default assigns from the prototype
[eva] using specification for function stop
[eva] Done for function stop
--
GitLab