adds src/plugins/variadic/tests (init)

src/plugins/variadic/.gitignore

 /configure
 /Makefile
-/tests/ptests_config
+/tests/**/dune
 /tests/*/result

src/plugins/variadic/tests/declared/called_in_ghost.i

 /* run.config
-   OPT: -kernel-warn-key ghost:bad-use=inactive -load-script tests/declared/called_in_ghost.ml -print
+   MODULE: @PTEST_NAME@.cmxs
+   OPT: -kernel-warn-key ghost:bad-use=inactive -print
 */
 // Note: we deactivate "ghost:bad-use" to check that printing goes right
 

src/plugins/variadic/tests/declared/oracle/called_in_ghost.res.oracle

-[kernel] Parsing tests/declared/called_in_ghost.i (no preprocessing)
+[kernel] Parsing called_in_ghost.i (no preprocessing)
 [kernel] function is not ghost
 [kernel] function is a non ghost global
 [kernel] e is a non ghost formal

src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle

-[variadic] tests/declared/empty-vpar-with-ghost.i:1: 
-  Declaration of variadic function f.
-[variadic] tests/declared/empty-vpar-with-ghost.i:8: 
+[variadic] empty-vpar-with-ghost.i:1: Declaration of variadic function f.
+[variadic] empty-vpar-with-ghost.i:8: 
   Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
-[kernel] tests/declared/empty-vpar-with-ghost.i:8: Warning: 
+[kernel] empty-vpar-with-ghost.i:8: Warning: 
   No code nor implicit assigns clause for function f, generating default assigns from the prototype
 [eva] using specification for function f
 [eva] done for function main

src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle

-[variadic] tests/declared/empty-vpar.i:1: Declaration of variadic function f.
-[variadic] tests/declared/empty-vpar.i:8: 
-  Generic translation of call to variadic function.
+[variadic] empty-vpar.i:1: Declaration of variadic function f.
+[variadic] empty-vpar.i:8: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
-[kernel] tests/declared/empty-vpar.i:8: Warning: 
+[kernel] empty-vpar.i:8: Warning: 
   No code nor implicit assigns clause for function f, generating default assigns from the prototype
 [eva] using specification for function f
 [eva] done for function main

src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle

-[variadic] tests/declared/function-ptr-with-ghost.i:4: 
-  Declaration of variadic function va_f.
-[variadic] tests/declared/function-ptr-with-ghost.i:2: 
+[variadic] function-ptr-with-ghost.i:4: Declaration of variadic function va_f.
+[variadic] function-ptr-with-ghost.i:2: 
   Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
-[kernel:annot:missing-spec] tests/declared/function-ptr-with-ghost.i:2: Warning: 
+[kernel:annot:missing-spec] function-ptr-with-ghost.i:2: Warning: 
   Neither code nor specification for function va_f, generating default assigns from the prototype
 [eva] using specification for function va_f
 [eva] done for function main

src/plugins/variadic/tests/declared/oracle/label.res.oracle

-[variadic] tests/declared/label.i:4: Declaration of variadic function f.
-[variadic] tests/declared/label.i:8: 
-  Generic translation of call to variadic function.
+[variadic] label.i:4: Declaration of variadic function f.
+[variadic] label.i:8: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
-[kernel:annot:missing-spec] tests/declared/label.i:8: Warning: 
+[kernel:annot:missing-spec] label.i:8: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
 [eva] using specification for function f
 [eva] done for function main

src/plugins/variadic/tests/declared/oracle/multi.res.oracle

-[variadic] tests/declared/multi.i:1: Declaration of variadic function f.
-[variadic] tests/declared/multi.i:12: Declaration of variadic function g.
-[variadic] tests/declared/multi.i:9: 
-  Generic translation of call to variadic function.
-[variadic] tests/declared/multi.i:18: 
-  Generic translation of call to variadic function.
+[variadic] multi.i:1: Declaration of variadic function f.
+[variadic] multi.i:12: Declaration of variadic function g.
+[variadic] multi.i:9: Generic translation of call to variadic function.
+[variadic] multi.i:18: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
-[kernel] tests/declared/multi.i:18: Warning: 
+[kernel] multi.i:18: Warning: 
   No code nor implicit assigns clause for function g, generating default assigns from the prototype
 [eva] using specification for function g
-[kernel] tests/declared/multi.i:9: Warning: 
+[kernel] multi.i:9: Warning: 
   No code nor implicit assigns clause for function f, generating default assigns from the prototype
 [eva] using specification for function f
 [eva] done for function main

src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle

 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
-[kernel:annot:missing-spec] tests/declared/no-va-with-ghost.i:4: Warning: 
+[kernel:annot:missing-spec] no-va-with-ghost.i:4: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
 [eva] using specification for function f
 [eva] done for function main

src/plugins/variadic/tests/declared/oracle/no-va.res.oracle

 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
-[kernel:annot:missing-spec] tests/declared/no-va.i:4: Warning: 
+[kernel:annot:missing-spec] no-va.i:4: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
 [eva] using specification for function f
 [eva] done for function main

src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle

-[variadic] tests/declared/rvalues-with-ghost.i:1: 
-  Declaration of variadic function f.
-[variadic] tests/declared/rvalues-with-ghost.i:5: 
+[variadic] rvalues-with-ghost.i:1: Declaration of variadic function f.
+[variadic] rvalues-with-ghost.i:5: 
   Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
-[kernel:annot:missing-spec] tests/declared/rvalues-with-ghost.i:5: Warning: 
+[kernel:annot:missing-spec] rvalues-with-ghost.i:5: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
 [eva] using specification for function f
 [eva] done for function main

src/plugins/variadic/tests/declared/oracle/rvalues.res.oracle

-[variadic] tests/declared/rvalues.i:1: Declaration of variadic function f.
-[variadic] tests/declared/rvalues.i:5: 
-  Generic translation of call to variadic function.
+[variadic] rvalues.i:1: Declaration of variadic function f.
+[variadic] rvalues.i:5: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
-[kernel:annot:missing-spec] tests/declared/rvalues.i:5: Warning: 
+[kernel:annot:missing-spec] rvalues.i:5: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
 [eva] using specification for function f
 [eva] done for function main

src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle

-[variadic] tests/declared/simple-with-ghost.i:1: 
-  Declaration of variadic function f.
-[variadic] tests/declared/simple-with-ghost.i:9: 
+[variadic] simple-with-ghost.i:1: Declaration of variadic function f.
+[variadic] simple-with-ghost.i:9: 
   Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
-[kernel] tests/declared/simple-with-ghost.i:9: Warning: 
+[kernel] simple-with-ghost.i:9: Warning: 
   No code nor implicit assigns clause for function f, generating default assigns from the prototype
 [eva] using specification for function f
 [eva] done for function main

src/plugins/variadic/tests/declared/oracle/simple.res.oracle

-[variadic] tests/declared/simple.i:1: Declaration of variadic function f.
-[variadic] tests/declared/simple.i:9: 
-  Generic translation of call to variadic function.
+[variadic] simple.i:1: Declaration of variadic function f.
+[variadic] simple.i:9: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
-[kernel] tests/declared/simple.i:9: Warning: 
+[kernel] simple.i:9: Warning: 
   No code nor implicit assigns clause for function f, generating default assigns from the prototype
 [eva] using specification for function f
 [eva] done for function main

src/plugins/variadic/tests/declared/oracle/struct.res.oracle

-[variadic] tests/declared/struct.i:5: Declaration of variadic function f.
-[variadic] tests/declared/struct.i:10: 
-  Generic translation of call to variadic function.
+[variadic] struct.i:5: Declaration of variadic function f.
+[variadic] struct.i:10: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
-[kernel:annot:missing-spec] tests/declared/struct.i:10: Warning: 
+[kernel:annot:missing-spec] struct.i:10: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
 [eva] using specification for function f
 [eva] done for function main

src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle

-[variadic] tests/declared/typedefed_function-with-ghost.i:2: 
+[variadic] typedefed_function-with-ghost.i:2: 
   Declaration of variadic function f.
-[variadic] tests/declared/typedefed_function-with-ghost.i:5: 
+[variadic] typedefed_function-with-ghost.i:5: 
   Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
-[kernel:annot:missing-spec] tests/declared/typedefed_function-with-ghost.i:5: Warning: 
+[kernel:annot:missing-spec] typedefed_function-with-ghost.i:5: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
 [eva] using specification for function f
 [eva] done for function main

src/plugins/variadic/tests/declared/oracle/typedefed_function.res.oracle

-[variadic] tests/declared/typedefed_function.i:2: 
-  Declaration of variadic function f.
-[variadic] tests/declared/typedefed_function.i:5: 
+[variadic] typedefed_function.i:2: Declaration of variadic function f.
+[variadic] typedefed_function.i:5: 
   Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
-[kernel:annot:missing-spec] tests/declared/typedefed_function.i:5: Warning: 
+[kernel:annot:missing-spec] typedefed_function.i:5: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
 [eva] using specification for function f
 [eva] done for function main

src/plugins/variadic/tests/defined/oracle/annot-formal.res.oracle

-[variadic] tests/defined/annot-formal.c:4: Declaration of variadic function sum.
-[variadic] tests/defined/annot-formal.c:20: 
-  Generic translation of call to variadic function.
+[variadic] annot-formal.c:4: Declaration of variadic function sum.
+[variadic] annot-formal.c:20: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed

src/plugins/variadic/tests/defined/oracle/annot-loc.res.oracle

-[variadic] tests/defined/annot-loc.c:4: Declaration of variadic function sum.
-[variadic] tests/defined/annot-loc.c:20: 
-  Generic translation of call to variadic function.
+[variadic] annot-loc.c:4: Declaration of variadic function sum.
+[variadic] annot-loc.c:20: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed

src/plugins/variadic/tests/defined/oracle/empty-vpar.res.oracle

-[variadic] tests/defined/empty-vpar.c:4: Declaration of variadic function sum.
-[variadic] tests/defined/empty-vpar.c:19: 
-  Generic translation of call to variadic function.
+[variadic] empty-vpar.c:4: Declaration of variadic function sum.
+[variadic] empty-vpar.c:19: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed