From fbce50cd62bb2551ea9f60338a531f276ecfe88a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 30 Sep 2020 18:49:56 +0200
Subject: [PATCH] Add execnow in ptests alias
---
ptests/ptests.ml | 10 ++++++++++
tests/float/absorb.c | 6 +++---
tests/float/oracle/absorb.res.oracle | 26 ++++++++++++++++++++++++--
tests/jcdb/jcdb.c | 2 +-
4 files changed, 38 insertions(+), 6 deletions(-)
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 274977fc09e..0a8c10a46d3 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -1716,6 +1716,7 @@ let dispatcher ~result_fmt ~oracle_fmt file directory config =
in
Format.fprintf result_fmt "\
(rule
+ (alias ptests)
(targets %a %a)
(action (system %S))
)
@@ -1724,6 +1725,15 @@ let dispatcher ~result_fmt ~oracle_fmt file directory config =
print_list res.ex_bin
res.ex_cmd
;
+ List.iter (fun log ->
+ Format.fprintf result_fmt
+ "(rule\n \
+ (alias ptests)\n \
+ (action (diff %S %S))\n\
+ )\n"
+ (Filename.concat ".." (Filename.concat SubDir.oracle_dirname log))
+ log
+ ) res.ex_log;
incr e
in
let treat_option option =
diff --git a/tests/float/absorb.c b/tests/float/absorb.c
index 0f89d00949a..7d284ad6cb7 100644
--- a/tests/float/absorb.c
+++ b/tests/float/absorb.c
@@ -1,8 +1,8 @@
/* run.config
COMMENT: run.config is intentionally not-*
- EXECNOW: BIN absorb.sav LOG absorb_sav.res LOG absorb_sav.err FRAMAC_PLUGIN=tests/.empty @frama-c@ -journal-disable -save absorb.sav @PTEST_FILE@ > absorb_sav.res 2> absorb_sav.err
- EXECNOW: BIN absorb.sav2 LOG absorb_sav2.res LOG absorb_sav2.err @frama-c@ -load absorb.sav -eva @EVA_CONFIG@ -journal-disable -float-hex -save absorb.sav2 > absorb_sav2.res 2> absorb_sav2.err
- OPT: -load absorb.sav2 -deps -out -input
+ EXECNOW: BIN absorb.sav LOG absorb_sav.res LOG absorb_sav.err PTESTS_IT_DOESNT_START_WITH_FRAMAC=yes @frama-c@ -no-autoload-plugins -journal-disable -save absorb.sav @PTEST_FILE@ > absorb_sav.res 2> absorb_sav.err
+ EXECNOW: BIN absorb.sav2 LOG absorb_sav2.res LOG absorb_sav2.err PTESTS_IT_DOESNT_START_WITH_FRAMAC=yes @frama-c@ -load %{dep:absorb.sav} -eva @EVA_CONFIG@ -journal-disable -float-hex -save absorb.sav2 > absorb_sav2.res 2> absorb_sav2.err
+ OPT: -load %{dep:absorb.sav2} -deps -out -input
*/
/* run.config*
DONTRUN:
diff --git a/tests/float/oracle/absorb.res.oracle b/tests/float/oracle/absorb.res.oracle
index 1b7a27a61e2..e65974a1604 100644
--- a/tests/float/oracle/absorb.res.oracle
+++ b/tests/float/oracle/absorb.res.oracle
@@ -1,2 +1,24 @@
-[kernel] User Error: Frama-C state file 'absorb.sav2' does not exist
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Warning: ignoring source files specified on the command line while loading a global initial context.
+[from] Computing for function main
+[from] Computing for function Frama_C_interval <-main
+[from] Done for function Frama_C_interval
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_interval:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ \result FROM Frama_C_entropy_source; min; max
+[from] Function main:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ x FROM x; y (and SELF)
+ y FROM x; y (and SELF)
+ z FROM y
+ t FROM Frama_C_entropy_source
+ min_f FROM \nothing
+ min_fl FROM \nothing
+ den FROM \nothing
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main:
+ Frama_C_entropy_source; x; y; z; t; min_f; min_fl; den; b; tmp
+[inout] Inputs for function main:
+ Frama_C_entropy_source; x; y; min_f
diff --git a/tests/jcdb/jcdb.c b/tests/jcdb/jcdb.c
index 87e5c8b9a6e..832434d3bfc 100644
--- a/tests/jcdb/jcdb.c
+++ b/tests/jcdb/jcdb.c
@@ -4,7 +4,7 @@ CMXS: @PTEST_NAME@
OPT: -json-compilation-database ./ -print
OPT: jcdb2.c -json-compilation-database with_arguments.json -print
OPT: -json-compilation-database with_arguments.json -load-module %{dep:@PTEST_NAME@.cmxs}
-EXECNOW: LOG list_files.res LOG list_files.err share/analysis-scripts/list_files.py compile_commands_working.json > list_files.res 2> list_files.err
+EXECNOW: LOG list_files.res LOG list_files.err %{read:../syntax/framac_share_path}/analysis-scripts/list_files.py %{dep:compile_commands_working.json} > list_files.res 2> list_files.err
*/
#include <stdio.h>
--
GitLab