[Ptests] migration of tests/specs

tests/ptests_config

@@ -5,12 +5,10 @@
 
 DEFAULT_SUITES= builtins callgraph cil constant_propagation dynamic fc_script float idct impact
 DEFAULT_SUITES= jcdb journal libc metrics misc occurrence pdg pretty_printing rte rte_manual
-DEFAULT_SUITES= saveload scope slicing sparecode syntax test value value/traces
+DEFAULT_SUITES= saveload scope slicing sparecode spec syntax test value value/traces
 
 # todo: adds make_run_script?
-# todo: adds spec (requires to fix wp tests)
 # todo: adds value/numerors (requires opam package mlgmpidl and system libraries for MPFR)
-IGNORE= DEFAULT_SUITES= spec
 IGNORE= DEFAULT_SUITES= make_run_script
 IGNORE= DEFAULT_SUITES= value/numerors
 

tests/spec/generalized_check.i

 /* run.config
+PLUGIN: @EVA_PLUGINS@
 OPT: -eva -eva-use-spec f
 OPT: -print
 */

tests/spec/multiple_include_2.c

 /* run.config
+   EXIT: 1
    DEPS: multiple_include.h
-   OPT: -kernel-warn-key=annot-error=active -print %{dep:multiple_include_1.c} -journal-disable
+   OPT: -kernel-warn-key=annot-error=active -print %{dep:multiple_include_1.c}
 */
+
 #include "multiple_include.h"
+
 /*@ requires p(x); */
 void bar(int x) { i+=x; return; }

tests/spec/oracle/generalized_check.0.res.oracle

-[kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
+[kernel] Parsing generalized_check.i (no preprocessing)
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva:alarm] tests/spec/generalized_check.i:23: Warning: 
+[eva:alarm] generalized_check.i:23: Warning: 
   accessing uninitialized left-value. assert \initialized(&c);
 [eva] using specification for function f
-[eva:alarm] tests/spec/generalized_check.i:24: Warning: 
+[eva:alarm] generalized_check.i:24: Warning: 
   function f: precondition 'f_valid_x' got status unknown.
-[eva] tests/spec/generalized_check.i:9: Warning: 
-  no \from part for clause 'assigns *x;'
-[eva:alarm] tests/spec/generalized_check.i:25: Warning: 
+[eva] generalized_check.i:9: Warning: no \from part for clause 'assigns *x;'
+[eva:alarm] generalized_check.i:25: Warning: 
   check 'main_valid_ko' got status unknown.
-[eva:alarm] tests/spec/generalized_check.i:26: Warning: 
+[eva:alarm] generalized_check.i:26: Warning: 
   check 'main_p_content_ko' got status unknown.
-[eva:alarm] tests/spec/generalized_check.i:32: Warning: 
+[eva:alarm] generalized_check.i:32: Warning: 
   loop invariant 'false_but_preserved' got status invalid.
-[eva] tests/spec/generalized_check.i:35: starting to merge loop iterations
-[eva:alarm] tests/spec/generalized_check.i:36: Warning: 
+[eva] generalized_check.i:35: starting to merge loop iterations
+[eva:alarm] generalized_check.i:36: Warning: 
   check 'implied_by_false_invariant' got status invalid.
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======