[tests] using PLUGIN directive and -no-autoload-plugins

src/plugins/aorai/tests/test_config

+PLUGIN: aorai eva,from,scope report wp,rtegen
+MODULE: aorai_test
 MACRO: PROVE_OPTIONS

src/plugins/aorai/tests/test_config_prove.in

+PLUGIN: aorai eva,from,scope report wp,rtegen
+MODULE: aorai_test
 MACRO: PROVE_OPTIONS @AORAI_WP_SHARE@ -aorai-test-prove-aux-spec

src/plugins/e-acsl/tests/test_config_ci.in

 MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
 MACRO: MACHDEP -machdep gcc_x86_64
 MACRO: GLOBAL @MACHDEP@ -remove-unused-specified-functions -verbose 0
+
 MACRO: EACSL -e-acsl -e-acsl-share ./share/e-acsl -e-acsl-verbose 1
 MACRO: EVA -eva -eva-no-alloc-returns-null -eva-no-results -eva-no-print -eva-warn-key libc:unsupported-spec=inactive
+
 MACRO: EVENTUALLY -print -ocode @DEST@.c -load-script ./tests/print.cmxs
+
+PLUGIN: E_ACSL eva,scope,variadic rtegen
+
 LOG: gen_@PTEST_NAME@.c
 OPT: @GLOBAL@ @EACSL@ -then-last @EVA@ @EVENTUALLY@
 FILTER:@SEDCMD@ -e "s|[a-zA-Z/\\]\+frama_c_project_e-acsl_[a-z0-9]*|PROJECT_FILE|" -e "s|$FRAMAC_SHARE|FRAMAC_SHARE|g" -e "s|../../share|FRAMAC_SHARE|g" -e "s|./share/e-acsl|FRAMAC_SHARE/e-acsl|g" -e "s|share/e-acsl|FRAMAC_SHARE/e-acsl|g"

src/plugins/e-acsl/tests/test_config_dev.in

@@ -12,7 +12,9 @@ MACRO: ROOT_EACSL_GCC_MISC_OPTS -q -X
 COMMENT: Default options for the frama-c invocation
 MACRO: ROOT_EACSL_GCC_FC_EXTRA -journal-disable -verbose 0
 
-EXEC: LOG @EACSL_ERR@ if test "@ROOT_EACSL_GCC_ENABLE@" = "yes"; then ./scripts/e-acsl-gcc.sh -I @frama-c@ -c @ROOT_EACSL_GCC_MISC_OPTS@ --frama-c-extra="@ROOT_EACSL_GCC_FC_EXTRA@ @ROOT_EACSL_GCC_FC_EXTRA_EXT@" @ROOT_EACSL_GCC_OPTS_EXT@ -o @DEST@.gcc.c -O @DEST@ @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl 2>&1 1>/dev/null | @ROOT_EACSL_EXEC_FILTER@ > @PTEST_RESULT@/@EACSL_ERR@; fi
+PLUGIN: E_ACSL eva,scope,variadic rtegen
+
+EXEC: LOG @EACSL_ERR@ if test "@ROOT_EACSL_GCC_ENABLE@" = "yes"; then ./scripts/e-acsl-gcc.sh -I @frama-c-exe@ -c @ROOT_EACSL_GCC_MISC_OPTS@ --frama-c-extra="@PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@ @ROOT_EACSL_GCC_FC_EXTRA@ @ROOT_EACSL_GCC_FC_EXTRA_EXT@" @ROOT_EACSL_GCC_OPTS_EXT@ -o @DEST@.gcc.c -O @DEST@ @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl 2>&1 1>/dev/null | @ROOT_EACSL_EXEC_FILTER@ > @PTEST_RESULT@/@EACSL_ERR@; fi
 
 COMMENT: These next macros can be redefined in a test file
 COMMENT: Define the following macro in a test to pass extra options to the frama-c invocation

src/plugins/instantiate/tests/test_config

+PLUGIN: instantiate

src/plugins/loop_analysis/tests/loop_analysis/with_value.i

 /*run.config
-OPT: -no-autoload-plugins -load-module from,inout,loopanalysis,eva,scope -eva -eva-show-progress -then -loop
+PLUGIN: from,inout,loopanalysis,eva,scope
+OPT: -eva -eva-show-progress -then -loop
 */
-
 void f1(int n) {
   for (int i = 1; i < n+2; i++); // i IN [1..6] (6)
 }

src/plugins/loop_analysis/tests/test_config

-OPT: -no-autoload-plugins -load-module loopanalysis -loop
+PLUGIN: loopanalysis
+OPT: -loop

src/plugins/markdown-report/tests/md/test_config

+PLUGIN: eva,inout,scope markdown_report
 CMD: @frama-c@ -eva @PTEST_FILE@ -mdr-gen md -mdr-date="now" -mdr-out @PTEST_DIR@/result/@PTEST_NAME@.@PTEST_NUMBER@.md
 LOG: @PTEST_NAME@.@PTEST_NUMBER@.md

src/plugins/markdown-report/tests/sarif/cwe125.c

@@ -4,8 +4,8 @@ EXECNOW: LOG @PTEST_NAME@.parse.log @frama-c@ @PTEST_FILE@ -save @PTEST_DIR@/res
 EXECNOW: LOG @PTEST_NAME@.eva.log @frama-c@ -load @PTEST_DIR@/result/@PTEST_NAME@_parse.sav -eva -save @PTEST_DIR@/result/@PTEST_NAME@_eva.sav > @PTEST_DIR@/result/@PTEST_NAME@.eva.log
 EXECNOW: LOG @PTEST_NAME@.sarif @frama-c@ -load @PTEST_DIR@/result/@PTEST_NAME@_eva.sav -then -mdr-out @PTEST_DIR@/result/@PTEST_NAME@.sarif -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic
 */
-#include "__fc_builtin.h"
 
+#include "__fc_builtin.h"
 #define LENGTH 10
 
 int getValueFromArray(int *array, int len, int index) {

src/plugins/markdown-report/tests/sarif/libc.c

 /* run.config
-   CMD: @frama-c@ @PTEST_FILE@ -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic
+   CMD: @frama-c@ -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic
    LOG: with-libc.sarif
    OPT: -mdr-out @PTEST_DIR@/result/with-libc.sarif
    LOG: without-libc.sarif

src/plugins/markdown-report/tests/sarif/oracle/cwe125.sarif

@@ -16,9 +16,11 @@
       "invocations": [
         {
           "commandLine":
-            "frama-c -check tests/sarif/cwe125.c -save tests/sarif/result/cwe125_parse.sav",
+            "frama-c -journal-disable -check -no-autoload-plugins -load-module=eva,from,scope,markdown_report tests/sarif/cwe125.c -save tests/sarif/result/cwe125_parse.sav",
           "arguments": [
-            "-check", "tests/sarif/cwe125.c", "-save",
+            "-journal-disable", "-check", "-no-autoload-plugins",
+            "-load-module=eva,from,scope,markdown_report",
+            "tests/sarif/cwe125.c", "-save",
             "tests/sarif/result/cwe125_parse.sav"
           ],
           "exitCode": 0,
@@ -26,21 +28,25 @@
         },
         {
           "commandLine":
-            "frama-c -check -load tests/sarif/result/cwe125_parse.sav -eva -save tests/sarif/result/cwe125_eva.sav",
+            "frama-c -journal-disable -check -no-autoload-plugins -load-module=eva,from,scope,markdown_report -load tests/sarif/result/cwe125_parse.sav -eva -save tests/sarif/result/cwe125_eva.sav",
           "arguments": [
-            "-check", "-load", "tests/sarif/result/cwe125_parse.sav", "-eva",
-            "-save", "tests/sarif/result/cwe125_eva.sav"
+            "-journal-disable", "-check", "-no-autoload-plugins",
+            "-load-module=eva,from,scope,markdown_report", "-load",
+            "tests/sarif/result/cwe125_parse.sav", "-eva", "-save",
+            "tests/sarif/result/cwe125_eva.sav"
           ],
           "exitCode": 0,
           "executionSuccessful": true
         },
         {
           "commandLine":
-            "frama-c -check -load tests/sarif/result/cwe125_eva.sav -then -mdr-out tests/sarif/result/cwe125.sarif -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic",
+            "frama-c -journal-disable -check -no-autoload-plugins -load-module=eva,from,scope,markdown_report -load tests/sarif/result/cwe125_eva.sav -then -mdr-out tests/sarif/result/cwe125.sarif -mdr-gen sarif -mdr-no-print-libc -mdr-sarif-deterministic",
           "arguments": [
-            "-check", "-load", "tests/sarif/result/cwe125_eva.sav", "-then",
-            "-mdr-out", "tests/sarif/result/cwe125.sarif", "-mdr-gen",
-            "sarif", "-mdr-no-print-libc", "-mdr-sarif-deterministic"
+            "-journal-disable", "-check", "-no-autoload-plugins",
+            "-load-module=eva,from,scope,markdown_report", "-load",
+            "tests/sarif/result/cwe125_eva.sav", "-then", "-mdr-out",
+            "tests/sarif/result/cwe125.sarif", "-mdr-gen", "sarif",
+            "-mdr-no-print-libc", "-mdr-sarif-deterministic"
           ],
           "exitCode": 0,
           "executionSuccessful": true

src/plugins/markdown-report/tests/sarif/oracle/std_string.sarif

@@ -16,9 +16,11 @@
       "invocations": [
         {
           "commandLine":
-            "frama-c -check tests/sarif/std_string.c -eva -then -mdr-sarif-deterministic -mdr-gen sarif -mdr-out tests/sarif/result/std_string.sarif",
+            "frama-c -journal-disable -check -no-autoload-plugins -load-module=eva,from,scope,markdown_report tests/sarif/std_string.c -eva -then -mdr-sarif-deterministic -mdr-gen sarif -mdr-out tests/sarif/result/std_string.sarif",
           "arguments": [
-            "-check", "tests/sarif/std_string.c", "-eva", "-then",
+            "-journal-disable", "-check", "-no-autoload-plugins",
+            "-load-module=eva,from,scope,markdown_report",
+            "tests/sarif/std_string.c", "-eva", "-then",
             "-mdr-sarif-deterministic", "-mdr-gen", "sarif", "-mdr-out",
             "tests/sarif/result/std_string.sarif"
           ],

src/plugins/markdown-report/tests/sarif/oracle/with-libc.sarif

@@ -16,12 +16,12 @@
       "invocations": [
         {
           "commandLine":
-            "frama-c -check tests/sarif/libc.c -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic -mdr-out tests/sarif/result/with-libc.sarif",
+            "frama-c -journal-disable -check -no-autoload-plugins -load-module=eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic tests/sarif/libc.c -mdr-out tests/sarif/result/with-libc.sarif",
           "arguments": [
-            "-check", "tests/sarif/libc.c", "-no-autoload-plugins",
-            "-load-module", "eva,from,scope,markdown_report", "-eva",
+            "-journal-disable", "-check", "-no-autoload-plugins",
+            "-load-module=eva,from,scope,markdown_report", "-eva",
             "-eva-no-results", "-mdr-gen", "sarif",
-            "-mdr-sarif-deterministic", "-mdr-out",
+            "-mdr-sarif-deterministic", "tests/sarif/libc.c", "-mdr-out",
             "tests/sarif/result/with-libc.sarif"
           ],
           "exitCode": 0,

src/plugins/markdown-report/tests/sarif/oracle/without-libc.sarif

@@ -16,12 +16,13 @@
       "invocations": [
         {
           "commandLine":
-            "frama-c -check tests/sarif/libc.c -no-autoload-plugins -load-module eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic -mdr-no-print-libc -mdr-out tests/sarif/result/without-libc.sarif",
+            "frama-c -journal-disable -check -no-autoload-plugins -load-module=eva,from,scope,markdown_report -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic tests/sarif/libc.c -mdr-no-print-libc -mdr-out tests/sarif/result/without-libc.sarif",
           "arguments": [
-            "-check", "tests/sarif/libc.c", "-no-autoload-plugins",
-            "-load-module", "eva,from,scope,markdown_report", "-eva",
+            "-journal-disable", "-check", "-no-autoload-plugins",
+            "-load-module=eva,from,scope,markdown_report", "-eva",
             "-eva-no-results", "-mdr-gen", "sarif",
-            "-mdr-sarif-deterministic", "-mdr-no-print-libc", "-mdr-out",
+            "-mdr-sarif-deterministic", "tests/sarif/libc.c",
+            "-mdr-no-print-libc", "-mdr-out",
             "tests/sarif/result/without-libc.sarif"
           ],
           "exitCode": 0,

src/plugins/markdown-report/tests/test_config

+PLUGIN: eva,from,scope markdown_report 

src/plugins/nonterm/tests/test_config

-OPT: -no-autoload-plugins -load-module from,inout,nonterm,scope -eva -eva-show-progress -eva-msg-key=-summary -then -nonterm -nonterm-verbose 2
+PLUGIN: from,inout,nonterm,scope
+OPT: -eva -eva-show-progress -eva-msg-key=-summary -then -nonterm -nonterm-verbose 2

src/plugins/report/tests/report/classify.c

 /* run.config
-   CMD: @frama-c@ -kernel-warn-key=annot-error=active -no-autoload-plugins -load-module wp,report -report-output @PTEST_RESULT@/classified.@PTEST_NUMBER@.json -wp -wp-msg-key shell
+   CMD: @frama-c@ -kernel-warn-key=annot-error=active -report-output @PTEST_RESULT@/classified.@PTEST_NUMBER@.json -wp -wp-msg-key shell
+PLUGIN: wp,rtegen,report
    LOG: classified.@PTEST_NUMBER@.json
    OPT: -wp-prover qed -report-unclassified-untried REVIEW -then -report-classify
 EXIT: 1
@@ -18,7 +19,6 @@ EXIT: 1
 int a ;
 
 
-
 /*@
   requires a >= 0 ;
   ensures a > 0 ;

src/plugins/report/tests/report/csv.c

 /* run.config
+PLUGIN: report from,inout,scope,eva
    LOG: csv.csv
-   OPT: -no-autoload-plugins -load-module from,inout,report,scope,eva -eva-warn-copy-indeterminate=-main4 -eva -eva-show-progress -eva-remove-redundant-alarms -eva-warn-key=alarm=inactive -then -report-csv @PTEST_RESULT@/csv.csv -report-no-proven -then -report-csv= -eva-warn-key=alarm -eva-slevel 1
+   OPT: -eva-warn-copy-indeterminate=-main4 -eva -eva-show-progress -eva-remove-redundant-alarms -eva-warn-key=alarm=inactive -then -report-csv @PTEST_RESULT@/csv.csv -report-no-proven -then -report-csv= -eva-warn-key=alarm -eva-slevel 1
    COMMENT: first, do an analysis without any message, but check that the .csv is complete. Then, redo the analysis with value warnings. slevel 1 is just there to force Value to restart
 */
 volatile v;
-
 void main1(int x) {
   int t[10];
   int u[15];

src/plugins/report/tests/report/hyp.i

 /* run.config
-   OPT: -no-autoload-plugins -load-module report -load-script tests/report/one_hyp.ml
-   OPT: -no-autoload-plugins -load-module report -load-script tests/report/several_hyps.ml
+   OPT: -load-script tests/report/one_hyp.ml
+   OPT: -load-script tests/report/several_hyps.ml
 */
 
 void f(void);

src/plugins/report/tests/report/single.i

 /* run.config
-   OPT: -no-autoload-plugins -load-module report -load-script tests/report/projectified_status.ml
-   OPT: -no-autoload-plugins -load-module report -load-script tests/report/no_hyp.ml
-   OPT: -no-autoload-plugins -load-module report -load-script tests/report/multi_emitters.ml
+   OPT: -load-script tests/report/projectified_status.ml
+   OPT: -load-script tests/report/no_hyp.ml
+   OPT: -load-script tests/report/multi_emitters.ml
 */
 
 void main() {