Merge branch 'feature/patrick/dunable-ptests' into 'master'

[ptests] Adds DEPS directive and accepts dune feature such as `%{dep:file}` in test commands

See merge request frama-c/frama-c!3475

src/plugins/wp/tests/wp_plugin/math.i

@@ -3,10 +3,10 @@
 */
 
 /* run.config_qualif
-   OPT: -wp-prover alt-ergo                                            -wp-prop=-ko  -wp-timeout 100 -wp-steps 1500
-   OPT: -wp-prover native:alt-ergo -wp-report=tests/native.report      -wp-prop=-ko  -wp-timeout 100 -wp-steps 1500
-   OPT: -wp-prover alt-ergo                                            -wp-prop=ko   -wp-timeout 100 -wp-steps 10
-   OPT: -wp-prover native:alt-ergo -wp-report=tests/native.report      -wp-prop=ko   -wp-timeout 100 -wp-steps 10
+   OPT: -wp-prover alt-ergo                                              -wp-prop=-ko  -wp-timeout 100 -wp-steps 1500
+   OPT: -wp-prover native:alt-ergo -wp-report=%{dep:tests/native.report} -wp-prop=-ko  -wp-timeout 100 -wp-steps 1500
+   OPT: -wp-prover alt-ergo                                              -wp-prop=ko   -wp-timeout 100 -wp-steps 10
+   OPT: -wp-prover native:alt-ergo -wp-report=%{dep:tests/native.report} -wp-prop=ko   -wp-timeout 100 -wp-steps 10
 */
 
 // --------------------------------------------------------------------------

src/plugins/wp/tests/wp_plugin/no_step_limit.i

@@ -2,10 +2,13 @@
   DONTRUN:
 */
 /* run.config_qualif
+ DEPS: @PTEST_NAME@.conf
   CMD: WHY3CONFIG=@PTEST_DIR@/@PTEST_NAME@.conf @frama-c@
   OPT: -wp -wp-prover no-steps -wp-steps 10 -wp-timeout 1 -wp-cache none -wp-no-cache-env -wp-msg-key shell
 */
+
 // cache is locally deactivated to see the option
+
 /*@
   lemma truc: \false ;
 */

src/plugins/wp/tests/wp_plugin/oracle/abs.res.oracle

@@ -6,7 +6,7 @@
   Function abs
 ------------------------------------------------------------
 
-Goal Post-condition (file tests/wp_plugin/abs.i, line 13) in 'abs':
+Goal Post-condition (file tests/wp_plugin/abs.i, line 15) in 'abs':
 Assume {
   Type: is_sint32(abs_0) /\ is_sint32(x).
   If x < 0

src/plugins/wp/tests/wp_plugin/region_to_coq.i

@@ -2,7 +2,7 @@
    DONTRUN:
 */
 /* run.config_qualif
-   OPT: -wp-prover native:coq -wp-coq-script tests/wp_plugin/region_to_coq.script
+   OPT: -wp-prover native:coq -wp-coq-script @PTEST_DIR@/region_to_coq.script
 */
 
 void copy(int* a, unsigned int n, int* b)

src/plugins/wp/tests/wp_region/annot.i

 /* run.config
    PLUGIN: wp
    OPT: -region-annot -print
-   EXECNOW: BIN ocode_@PTEST_NAME@_1.i @frama-c@ @PTEST_DIR@/@PTEST_NAME@.i            -region-annot -print -ocode @PTEST_RESULT@/ocode_@PTEST_NAME@_1.i > @DEV_NULL@ 2> @DEV_NULL@
-   EXECNOW: BIN ocode_@PTEST_NAME@_2.i @frama-c@ @PTEST_RESULT@/ocode_@PTEST_NAME@_1.i -region-annot -print -ocode @PTEST_RESULT@/ocode_@PTEST_NAME@_2.i > @DEV_NULL@ 2> @DEV_NULL@
-   EXECNOW: LOG  diff_@PTEST_NAME@.txt diff @PTEST_RESULT@/ocode_@PTEST_NAME@_1.i @PTEST_RESULT@/ocode_@PTEST_NAME@_2.i &> @PTEST_RESULT@/diff_@PTEST_NAME@.txt
+   EXECNOW: BIN ocode_@PTEST_NAME@_1.i @frama-c@ %{dep:@PTEST_DIR@/@PTEST_NAME@.i}            -region-annot -print -ocode @PTEST_RESULT@/ocode_@PTEST_NAME@_1.i > @DEV_NULL@ 2> @DEV_NULL@
+   EXECNOW: BIN ocode_@PTEST_NAME@_2.i @frama-c@ %{dep:@PTEST_RESULT@/ocode_@PTEST_NAME@_1.i} -region-annot -print -ocode @PTEST_RESULT@/ocode_@PTEST_NAME@_2.i > @DEV_NULL@ 2> @DEV_NULL@
+   EXECNOW: LOG  diff_@PTEST_NAME@.txt diff %{dep:@PTEST_RESULT@/ocode_@PTEST_NAME@_1.i} %{dep:@PTEST_RESULT@/ocode_@PTEST_NAME@_2.i} &> @PTEST_RESULT@/diff_@PTEST_NAME@.txt
 COMMENT: The file diff_@PTEST_NAME@.txt must be empty.
 COMMENT: So, that file has not to be present into the oracle directory since absent files are considered such as empty files.
  */

src/plugins/wp/tests/wp_typed/unit_bitwise.c

 /* run.config
+ DEPS: unit_bitwise.h
    OPT:
 */
 /* run.config_qualif
+ DEPS: unit_bitwise.h
    OPT: -wp-prop="-ko"
    OPT: -wp-prop="ko"
 */
 
-
-
 #include "unit_bitwise.h"
 //===============================================
 //-- int

src/plugins/wp/tests/wp_usage/save_load.i

 /* run.config
-   EXECNOW: LOG save_load.sav.res LOG save_load.sav.err BIN @PTEST_NAME@.sav @frama-c@ -wp-warn-key pedantic-assigns=inactive -wp-share ./share -wp -wp-print -wp-prover none @PTEST_FILE@ -save @PTEST_DIR@/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@.sav.res 2> @PTEST_DIR@/result/@PTEST_NAME@.sav.err
-   CMD: @frama-c@ -load @PTEST_DIR@/@PTEST_NAME@.sav -wp-warn-key pedantic-assigns=inactive
+   EXECNOW: LOG save_load.sav.res LOG save_load.sav.err BIN @PTEST_NAME@.sav @frama-c@ -wp-warn-key pedantic-assigns=inactive -wp-share ./share -wp -wp-print -wp-prover none @PTEST_FILE@ -save @PTEST_RESULT@/@PTEST_NAME@.sav > @PTEST_RESULT@/@PTEST_NAME@.sav.res 2> @PTEST_RESULT@/@PTEST_NAME@.sav.err
+   CMD: @frama-c@ -load %{dep:@PTEST_RESULT@/@PTEST_NAME@.sav} -wp-warn-key pedantic-assigns=inactive
    OPT: -print
    OPT: -wp -wp-prover none -wp-print
 */

tests/cil/cpu_a.c

 /* run.config
-   OPT: tests/cil/cpu_b.c -machdep x86_16 -print
+   OPT: %{dep:@PTEST_DIR@/cpu_b.c} -machdep x86_16 -print
 */
 typedef unsigned short DWORD ;
 

tests/cil/cpu_b.c

 /* run.config
-   OPT: tests/cil/cpu_a.c -machdep x86_16 -print
+   OPT:  %{dep:@PTEST_DIR@/cpu_a.c} -machdep x86_16 -print
 */
 
 typedef unsigned int DWORD ;

tests/cil/merge.c

 /* run.config
-   OPT: tests/cil/merge2.c -print
+   STDOPT: +"%{dep:@PTEST_DIR@/merge2.c}"
 */
 extern int x;

tests/cil/merge2.c

 /* run.config
-   OPT: tests/cil/merge.c -print
+   STDOPT: +"%{dep:@PTEST_DIR@/merge.c}"
  */
 int x =2;

tests/dynamic/dynamic.i

 /*run.config
-  OPT: -add-path tests/dynamic/file_path -add-path tests/dynamic/directory_path -add-path tests/dynamic/none
+  OPT: -add-path @PTEST_DIR@/file_path -add-path @PTEST_DIR@/directory_path -add-path @PTEST_DIR@/none
  MODULE: empty abstract abstract2
   OPT:
  */

tests/fc_script/build-callgraph.i

 /* run.config
    NOFRAMAC: testing frama-c-script, not frama-c itself
-   EXECNOW: LOG build-callgraph.res LOG build-callgraph.err bin/frama-c-script heuristic-print-callgraph @PTEST_DIR@/@PTEST_NAME@.i > @PTEST_DIR@/result/build-callgraph.res 2> @PTEST_DIR@/result/build-callgraph.err
+   EXECNOW: LOG build-callgraph.res LOG build-callgraph.err bin/frama-c-script heuristic-print-callgraph @PTEST_DIR@/@PTEST_NAME@.i > @PTEST_RESULT@/build-callgraph.res 2> @PTEST_RESULT@/build-callgraph.err
  */
 
 #include <stdio.h>

tests/fc_script/list_functions.i

 /* run.config
-   NOFRAMAC: testing frama-c-script, not frama-c itself
-   EXECNOW: LOG heuristic_list_functions.res LOG heuristic_list_functions.err bin/frama-c-script heuristic-list-functions true true @PTEST_DIR@/*.c @PTEST_DIR@/*.i > @PTEST_DIR@/result/heuristic_list_functions.res 2> @PTEST_DIR@/result/heuristic_list_functions.err
+ NOFRAMAC: testing frama-c-script, not frama-c itself
+
+ DEPS: @PTEST_DEPS@ @PTEST_DIR@/for-find-fun.c
+ DEPS: @PTEST_DEPS@ @PTEST_DIR@/for-find-fun2.c
+ DEPS: @PTEST_DEPS@ @PTEST_DIR@/for-list-functions.c
+ DEPS: @PTEST_DEPS@ @PTEST_DIR@/list_functions.i
+ DEPS: @PTEST_DEPS@ @PTEST_DIR@/main.c
+ DEPS: @PTEST_DEPS@ @PTEST_DIR@/main2.c
+ DEPS: @PTEST_DEPS@ @PTEST_DIR@/main3.c
+ DEPS: @PTEST_DEPS@ @PTEST_DIR@/make-wrapper.c
+ DEPS: @PTEST_DEPS@ @PTEST_DIR@/make-wrapper2.c
+ DEPS: @PTEST_DEPS@ @PTEST_DIR@/make-wrapper3.c
+
+ DEPS: @PTEST_DEPS@ @PTEST_DIR@/build-callgraph.i
+ DEPS: @PTEST_DEPS@ @PTEST_DIR@/recursions.i
+
+   EXECNOW: LOG heuristic_list_functions.res LOG heuristic_list_functions.err %{bin:frama-c-script} heuristic-list-functions true true @PTEST_DEPS@ > @PTEST_RESULT@/heuristic_list_functions.res 2> @PTEST_RESULT@/heuristic_list_functions.err
  */

tests/fc_script/main.c

 /* run.config
-   NOFRAMAC: testing frama-c-script, not frama-c itself
-   EXECNOW: LOG GNUmakefile LOG make_template.res LOG make_template.err cd @PTEST_DIR@ && PTESTS_TESTING= ../../bin/frama-c-script make-template result < make_template.input > result/make_template.res 2> result/make_template.err
-   EXECNOW: LOG list_files.res LOG list_files.err bin/frama-c-script list-files @PTEST_DIR@/list_files.json > @PTEST_DIR@/result/list_files.res 2> @PTEST_DIR@/result/list_files.err
-   EXECNOW: LOG find_fun1.res LOG find_fun1.err bin/frama-c-script find-fun main2 @PTEST_DIR@ > @PTEST_DIR@/result/find_fun1.res 2> @PTEST_DIR@/result/find_fun1.err
-   EXECNOW: LOG find_fun2.res LOG find_fun2.err bin/frama-c-script find-fun main3 @PTEST_DIR@ > @PTEST_DIR@/result/find_fun2.res 2> @PTEST_DIR@/result/find_fun2.err
-   EXECNOW: LOG find_fun3.res LOG find_fun3.err bin/frama-c-script find-fun false_positive @PTEST_DIR@ > @PTEST_DIR@/result/find_fun3.res 2> @PTEST_DIR@/result/find_fun3.err
-   EXECNOW: LOG list_functions.res LOG list_functions.err bin/frama-c-script list-functions @PTEST_DIR@/for-find-fun2.c @PTEST_DIR@/for-list-functions.c > @PTEST_DIR@/result/list_functions.res 2> @PTEST_DIR@/result/list_functions.err
-   EXECNOW: LOG list_functions2.res LOG list_functions2.err LOG list_functions2.json bin/frama-c-script list-functions @PTEST_DIR@/for-find-fun2.c @PTEST_DIR@/for-list-functions.c -list-functions-declarations -list-functions-output @PTEST_DIR@/result/list_functions2.json -list-functions-debug 1 > @PTEST_DIR@/result/list_functions2.res 2> @PTEST_DIR@/result/list_functions2.err
+ NOFRAMAC: testing frama-c-script, not frama-c itself
+ DEPS: for-find-fun2.c for-find-fun.c main.c main2.c main3.c
+   EXECNOW: LOG GNUmakefile LOG make_template.res LOG make_template.err PTESTS_TESTING= %{bin:frama-c-script} -C @PTEST_DIR@ make-template result < %{dep:@PTEST_DIR@/make_template.input} > @PTEST_RESULT@/make_template.res 2> @PTEST_RESULT@/make_template.err
+ DEPS: main2.c main3.c main.c
+   EXECNOW: LOG list_files.res LOG list_files.err %{bin:frama-c-script} list-files %{dep:@PTEST_DIR@/list_files.json} > @PTEST_RESULT@/list_files.res 2> @PTEST_RESULT@/list_files.err
+ DEPS: for-find-fun2.c for-find-fun.c for-list-functions.c main2.c main3.c main.c make-wrapper2.c make-wrapper3.c make-wrapper.c
+   EXECNOW: LOG find_fun1.res LOG find_fun1.err %{bin:frama-c-script} find-fun main2 @PTEST_DIR@ > @PTEST_RESULT@/find_fun1.res 2> @PTEST_RESULT@/find_fun1.err
+   EXECNOW: LOG find_fun2.res LOG find_fun2.err %{bin:frama-c-script} find-fun main3 @PTEST_DIR@ > @PTEST_RESULT@/find_fun2.res 2> @PTEST_RESULT@/find_fun2.err
+   EXECNOW: LOG find_fun3.res LOG find_fun3.err %{bin:frama-c-script} find-fun false_positive @PTEST_DIR@ > @PTEST_RESULT@/find_fun3.res 2> @PTEST_RESULT@/find_fun3.err
+ DEPS:
+   EXECNOW: LOG list_functions.res LOG list_functions.err %{bin:frama-c-script} list-functions %{dep:@PTEST_DIR@/for-find-fun2.c} %{dep:@PTEST_DIR@/for-list-functions.c} > @PTEST_RESULT@/list_functions.res 2> @PTEST_RESULT@/list_functions.err
+   EXECNOW: LOG list_functions2.res LOG list_functions2.err LOG list_functions2.json %{bin:frama-c-script} list-functions %{dep:@PTEST_DIR@/for-find-fun2.c} %{dep:@PTEST_DIR@/for-list-functions.c -list-functions-declarations} -list-functions-output @PTEST_RESULT@/list_functions2.json -list-functions-debug 1 > @PTEST_RESULT@/list_functions2.res 2> @PTEST_RESULT@/list_functions2.err
  */
 
+
+
 void main() {
 
 }
+// NB: Dependency to ./share directory where are script files used by %{bin:frama-c-script} is implicit with `dune` testing.

tests/fc_script/oracle/heuristic_list_functions.res

@@ -7,7 +7,7 @@ tests/fc_script/for-find-fun2.c:19:21: h (definition)
 tests/fc_script/for-find-fun2.c:28:31: static_fun (definition)
 tests/fc_script/for-list-functions.c:8:15: static_fun (definition)
 tests/fc_script/for-list-functions.c:17:22: k (definition)
-tests/fc_script/main.c:12:14: main (definition)
+tests/fc_script/main.c:18:20: main (definition)
 tests/fc_script/main2.c:6:8: fake_main (definition)
 tests/fc_script/main2.c:10:12: domain (definition)
 tests/fc_script/main2.c:14:16: main2 (definition)

tests/fc_script/recursions.i

 /* run.config
    NOFRAMAC: testing frama-c-script, not frama-c itself
-   EXECNOW: LOG recursions.res LOG recursions.err bin/frama-c-script heuristic-detect-recursion @PTEST_FILE@ > @PTEST_DIR@/result/recursions.res 2> @PTEST_DIR@/result/recursions.err
+   EXECNOW: LOG recursions.res LOG recursions.err bin/frama-c-script heuristic-detect-recursion @PTEST_FILE@ > @PTEST_RESULT@/recursions.res 2> @PTEST_RESULT@/recursions.err
 */
 
 volatile int v;

tests/float/absorb.c

 /* run.config
    COMMENT: run.config is intentionally not-*
 PLUGIN:
-   EXECNOW: BIN absorb.sav LOG absorb_sav.res LOG absorb_sav.err @frama-c@ -save @PTEST_DIR@/result/absorb.sav @PTEST_FILE@ > @PTEST_DIR@/result/absorb_sav.res 2> @PTEST_DIR@/result/absorb_sav.err
+   EXECNOW: BIN absorb.sav LOG absorb_sav.res LOG absorb_sav.err @frama-c@ -save @PTEST_RESULT@/absorb.sav @PTEST_FILE@ > @PTEST_RESULT@/absorb_sav.res 2> @PTEST_RESULT@/absorb_sav.err
 PLUGIN: @EVA_PLUGINS@
-   EXECNOW: BIN absorb.sav2 LOG absorb_sav2.res LOG absorb_sav2.err @frama-c@ -load @PTEST_DIR@/result/absorb.sav -eva @EVA_CONFIG@ -float-hex -save @PTEST_DIR@/result/absorb.sav2 > @PTEST_DIR@/result/absorb_sav2.res 2> @PTEST_DIR@/result/absorb_sav2.err
-   OPT: -load @PTEST_DIR@/result/absorb.sav2 -deps -out -input
+   EXECNOW: BIN absorb.sav2 LOG absorb_sav2.res LOG absorb_sav2.err @frama-c@ -load %{dep:@PTEST_RESULT@/absorb.sav} -eva @EVA_CONFIG@ -float-hex -save @PTEST_RESULT@/absorb.sav2 > @PTEST_RESULT@/absorb_sav2.res 2> @PTEST_RESULT@/absorb_sav2.err
+   OPT: -load %{dep:@PTEST_RESULT@/absorb.sav2} -deps -out -input
 */
 /* run.config*
    DONTRUN:

tests/idct/ieee_1180_1990.c

 /* run.config*
-  PLUGIN: @PTEST_PLUGIN@ report   
-   STDOPT: +"-eva-msg-key=summary -float-normal -no-warn-signed-overflow tests/idct/idct.c -eva-remove-redundant-alarms -eva-memexec -eva-builtin sqrt:Frama_C_sqrt,cos:Frama_C_cos -then -report -report-print-properties"
+ PLUGIN: @PTEST_PLUGIN@ report
+   STDOPT: +"-eva-msg-key=summary -float-normal -no-warn-signed-overflow %{dep:@PTEST_DIR@/idct.c} -eva-remove-redundant-alarms -eva-memexec -eva-builtin sqrt:Frama_C_sqrt,cos:Frama_C_cos -then -report -report-print-properties"
 */
 /* IEEE_1180_1990: a testbed for IDCT accuracy
  * Copyright (C) 2001  Renaud Pacalet

tests/jcdb/jcdb.c

 /* run.config
+ DEPS: compile_commands.json
+ COMMENT: parsing option are defined in the default json file "compile_commands.json"
    OPT: -json-compilation-database @PTEST_DIR@ -print
-   OPT: @PTEST_DIR@/jcdb2.c -json-compilation-database @PTEST_DIR@/with_arguments.json -print
+ DEPS:
+   OPT: %{dep:@PTEST_DIR@/jcdb2.c} -json-compilation-database %{dep:@PTEST_DIR@/with_arguments.json} -print
  MODULE: @PTEST_NAME@
-   OPT: -json-compilation-database @PTEST_DIR@/with_arguments.json -no-autoload-plugins
+   OPT: -json-compilation-database %{dep:@PTEST_DIR@/with_arguments.json}
  MODULE:
-   EXECNOW: LOG list_files.res LOG list_files.err share/analysis-scripts/list_files.py @PTEST_DIR@/compile_commands_working.json > @PTEST_DIR@/result/list_files.res 2> @PTEST_DIR@/result/list_files.err
-   EXECNOW: LOG logic-pp-include.res LOG logic-pp-include.err @frama-c@ -json-compilation-database @PTEST_DIR@/logic-pp-include @PTEST_DIR@/logic-pp-include/no-stdio.c -print > @PTEST_DIR@/result/logic-pp-include.res 2> @PTEST_DIR@/result/logic-pp-include.err
+   EXECNOW: LOG list_files.res LOG list_files.err %{bin:frama-c-script} list-files %{dep:@PTEST_DIR@/compile_commands_working.json} > @PTEST_RESULT@/list_files.res 2> @PTEST_RESULT@/list_files.err
 */
 
 #include <stdio.h>