[Tests] add test config qualif of wp (init)

Makefile

@@ -182,7 +182,7 @@ TESTS=builtins callgraph cil constant_propagation dynamic float idct impact jcdb
 
 # todo: adds aorai (2 configs + Aorai_test library)
 # todo: no test found for studia ?
-# todo: adds wp (at least 2 configs)
+# todo: adds wp (config qualif)
 PLUGIN_TESTS= dive instantiate loop_analysis markdown-report nonterm report server variadic wp
 
 tests: config.sed

src/plugins/wp/tests/test_config_qualif

-CMD: @frama-c@ -wp -wp-par 1 -wp-share ../../../share -wp-msg-key shell -wp-report  %{dep:../../qualif.report} -wp-session @PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@ -wp-coq-timeout 120
+PLUGIN: wp,rtegen
+CMD: @frama-c@ -wp -wp-par 1 -wp-share ../../../share -wp-msg-key shell -wp-report  %{dep:../../qualif.report} -wp-session @PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay -wp-coq-timeout 120
 OPT:

src/plugins/wp/tests/wp/oracle_qualif/cfg_loop.res.oracle

 # frama-c -wp [...]
-[kernel] Parsing tests/wp/cfg_loop.i (no preprocessing)
+[kernel] Parsing cfg_loop.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 15 goals scheduled

src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle

 # frama-c -wp [...]
-[kernel] Parsing tests/wp/sharing.c (with preprocessing)
+[kernel] Parsing sharing.c (with preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled

src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle

 # frama-c -wp [...]
-[kernel] Parsing tests/wp/stmtcompiler_test.i (no preprocessing)
-[kernel] tests/wp/stmtcompiler_test.i:136: Warning: 
+[kernel] Parsing stmtcompiler_test.i (no preprocessing)
+[kernel] stmtcompiler_test.i:136: Warning: 
   Body of function if_assert falls-through. Adding a return statement
 [wp] Running WP plugin...
-[kernel] tests/wp/stmtcompiler_test.i:145: Warning: 
+[kernel] stmtcompiler_test.i:145: Warning: 
   No code nor implicit assigns clause for function behavior1, generating default assigns from the prototype
 [wp] Warning: Missing RTE guards
-[wp] tests/wp/stmtcompiler_test.i:81: Warning: 
+[wp] stmtcompiler_test.i:81: Warning: 
   Missing assigns clause (assigns 'everything' instead)
 [wp] 27 goals scheduled
 [wp] [Qed] Goal typed_empty_assert : Valid

src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test_rela.res.oracle

 # frama-c -wp [...]
-[kernel] Parsing tests/wp/stmtcompiler_test_rela.i (no preprocessing)
+[kernel] Parsing stmtcompiler_test_rela.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled

src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle

 # frama-c -wp -wp-timeout 1 [...]
-[kernel] Parsing tests/wp/wp_behav.c (with preprocessing)
+[kernel] Parsing wp_behav.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] tests/wp/wp_behav.c:172: Warning: 
+[wp] wp_behav.c:172: Warning: 
   Ignored specification 'for b1' (generalize to all behavior)
 [wp] Warning: Missing RTE guards
-[wp] tests/wp/wp_behav.c:69: Warning: 
+[wp] wp_behav.c:69: Warning: 
   Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp/wp_behav.c:81: Warning: 
+[wp] wp_behav.c:81: Warning: 
   Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp/wp_behav.c:154: Warning: 
+[wp] wp_behav.c:154: Warning: 
   Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp/wp_behav.c:176: Warning: 
+[wp] wp_behav.c:176: Warning: 
   Missing assigns clause (assigns 'everything' instead)
 [wp] 38 goals scheduled
 [wp] [Qed] Goal typed_f_ensures_qed_ok : Valid

src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle

 # frama-c -wp -wp-steps 50 [...]
-[kernel] Parsing tests/wp/wp_behav.c (with preprocessing)
+[kernel] Parsing wp_behav.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] tests/wp/wp_behav.c:172: Warning: 
+[wp] wp_behav.c:172: Warning: 
   Ignored specification 'for b1' (generalize to all behavior)
 [wp] Warning: Missing RTE guards
-[wp] tests/wp/wp_behav.c:69: Warning: 
+[wp] wp_behav.c:69: Warning: 
   Missing assigns clause (assigns 'everything' instead)
 [wp] 8 goals scheduled
 [wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko : Unsuccess

src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle

 # frama-c -wp [...]
-[kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing)
+[kernel] Parsing wp_call_pre.c (with preprocessing)
 [wp] Running WP plugin...
-[kernel] tests/wp/wp_call_pre.c:53: Warning: 
+[kernel] wp_call_pre.c:53: Warning: 
   No code nor implicit assigns clause for function f, generating default assigns from the prototype
-[kernel] tests/wp/wp_call_pre.c:53: Warning: 
+[kernel] wp_call_pre.c:53: Warning: 
   No code nor implicit assigns clause for function g, generating default assigns from the prototype
 [wp] Warning: Missing RTE guards
 [wp] 10 goals scheduled

src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle

 # frama-c -wp [...]
-[kernel] Parsing tests/wp/wp_eqb.i (no preprocessing)
+[kernel] Parsing wp_eqb.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled

src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle

 # frama-c -wp -wp-model 'Hoare' [...]
-[kernel] Parsing tests/wp/wp_strategy.c (with preprocessing)
+[kernel] Parsing wp_strategy.c (with preprocessing)
 [rte] annotating function bts0513
 [rte] annotating function bts0513_bis
 [rte] annotating function default_behaviors

src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle

 # frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/arith.i (no preprocessing)
+[kernel] Parsing arith.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 24 goals scheduled

src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle

 # frama-c -wp -wp-steps 50 [...]
-[kernel] Parsing tests/wp_acsl/arith.i (no preprocessing)
+[kernel] Parsing arith.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled

src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle

 # frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/assign_array.i (no preprocessing)
+[kernel] Parsing assign_array.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 4 goals scheduled

src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.res.oracle

 # frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/assigned_initialized_memtyped.i (no preprocessing)
+[kernel] Parsing assigned_initialized_memtyped.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 42 goals scheduled

src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle

 # frama-c -wp -wp-timeout 20 [...]
-[kernel] Parsing tests/wp_acsl/assigned_initialized_memvar.i (no preprocessing)
+[kernel] Parsing assigned_initialized_memvar.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 22 goals scheduled

src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_not_initialized_memtyped.res.oracle

 # frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/assigned_not_initialized_memtyped.i (no preprocessing)
+[kernel] Parsing assigned_not_initialized_memtyped.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 9 goals scheduled

src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_not_initialized_memvar.res.oracle

 # frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/assigned_not_initialized_memvar.i (no preprocessing)
+[kernel] Parsing assigned_not_initialized_memvar.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 3 goals scheduled

src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle

 # frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/assigns_path.i (no preprocessing)
+[kernel] Parsing assigns_path.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 9 goals scheduled

src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle

 # frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/assigns_range.i (no preprocessing)
+[kernel] Parsing assigns_range.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 [wp] 17 goals scheduled