From 03ad796baac3c4fb63848deb4aedb7c3071e91d1 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 2 Oct 2020 08:22:54 +0200
Subject: [PATCH] adds src/plugins/variadic/tests (init)
---
src/plugins/variadic/.gitignore | 2 +-
.../variadic/tests/declared/called_in_ghost.i | 3 +-
.../oracle/called_in_ghost.res.oracle | 2 +-
.../oracle/empty-vpar-with-ghost.res.oracle | 7 +-
.../declared/oracle/empty-vpar.res.oracle | 7 +-
.../oracle/function-ptr-with-ghost.res.oracle | 7 +-
.../tests/declared/oracle/label.res.oracle | 7 +-
.../tests/declared/oracle/multi.res.oracle | 14 +--
.../oracle/no-va-with-ghost.res.oracle | 2 +-
.../tests/declared/oracle/no-va.res.oracle | 2 +-
.../oracle/rvalues-with-ghost.res.oracle | 7 +-
.../tests/declared/oracle/rvalues.res.oracle | 7 +-
.../oracle/simple-with-ghost.res.oracle | 7 +-
.../tests/declared/oracle/simple.res.oracle | 7 +-
.../tests/declared/oracle/struct.res.oracle | 7 +-
.../typedefed_function-with-ghost.res.oracle | 6 +-
.../oracle/typedefed_function.res.oracle | 7 +-
.../defined/oracle/annot-formal.res.oracle | 5 +-
.../tests/defined/oracle/annot-loc.res.oracle | 5 +-
.../defined/oracle/empty-vpar.res.oracle | 5 +-
.../tests/defined/oracle/forward.res.oracle | 5 +-
.../tests/defined/oracle/max.res.oracle | 5 +-
.../oracle/multiple-va_start.res.oracle | 8 +-
.../defined/oracle/pointers-to-va.res.oracle | 13 +-
.../tests/defined/oracle/recursive.res.oracle | 15 +--
.../tests/defined/oracle/sentinel.res.oracle | 5 +-
.../tests/defined/oracle/simple.res.oracle | 5 +-
.../tests/defined/oracle/struct.res.oracle | 5 +-
.../tests/defined/oracle/va_copy.res.oracle | 7 +-
.../defined/oracle/va_list-as-arg.res.oracle | 5 +-
.../tests/erroneous/oracle/exec.res.oracle | 21 ++--
.../erroneous/oracle/invalid_libc.res.oracle | 8 +-
.../tests/erroneous/oracle/no-libc.res.oracle | 4 +-
.../oracle/not-enough-par.res.oracle | 5 +-
.../tests/erroneous/oracle/printf.res.oracle | 7 +-
.../oracle/va_arg-wrongtype.res.oracle | 7 +-
.../oracle/variadic-builtin.res.oracle | 2 +-
.../variadic/tests/erroneous/test_config | 2 +-
.../tests/known/oracle/exec.res.oracle | 21 ++--
.../oracle/exec_failed_requirement.res.oracle | 4 +-
.../tests/known/oracle/fcntl.res.oracle | 24 ++--
.../tests/known/oracle/ioctl.res.oracle | 10 +-
.../tests/known/oracle/open.res.oracle | 11 +-
.../tests/known/oracle/open_wrong.res.oracle | 5 +-
.../tests/known/oracle/openat.res.oracle | 11 +-
.../tests/known/oracle/print_libc.res.oracle | 6 +-
.../tests/known/oracle/printf.res.oracle | 63 +++++-----
.../oracle/printf_garbled_mix.res.oracle | 16 ++-
.../known/oracle/printf_redefined.res.oracle | 7 +-
.../oracle/printf_wrong_arity.res.oracle | 12 +-
.../oracle/printf_wrong_pointers.res.oracle | 16 +--
.../oracle/printf_wrong_types.res.oracle | 116 +++++++++---------
.../tests/known/oracle/scanf.res.oracle | 2 +-
.../tests/known/oracle/scanf_loop.res.oracle | 2 +-
.../tests/known/oracle/scanf_wrong.res.oracle | 9 +-
.../tests/known/oracle/snprintf.res.oracle | 10 +-
.../tests/known/oracle/stdio_print.res.oracle | 42 +++----
.../tests/known/oracle/stdio_scan.res.oracle | 26 ++--
.../tests/known/oracle/swprintf.res.oracle | 10 +-
.../tests/known/oracle/wchar.res.oracle | 20 +--
src/plugins/variadic/tests/known/print_libc.c | 2 +-
src/plugins/variadic/tests/ptests_config | 1 +
src/plugins/variadic/tests/test_config | 3 +-
63 files changed, 318 insertions(+), 376 deletions(-)
create mode 100644 src/plugins/variadic/tests/ptests_config
diff --git a/src/plugins/variadic/.gitignore b/src/plugins/variadic/.gitignore
index 0114e3d0f08..b18adc61b4f 100644
--- a/src/plugins/variadic/.gitignore
+++ b/src/plugins/variadic/.gitignore
@@ -1,4 +1,4 @@
/configure
/Makefile
-/tests/ptests_config
+/tests/**/dune
/tests/*/result
diff --git a/src/plugins/variadic/tests/declared/called_in_ghost.i b/src/plugins/variadic/tests/declared/called_in_ghost.i
index 7d6ccc4f7f6..31352e2ab42 100644
--- a/src/plugins/variadic/tests/declared/called_in_ghost.i
+++ b/src/plugins/variadic/tests/declared/called_in_ghost.i
@@ -1,5 +1,6 @@
/* 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
diff --git a/src/plugins/variadic/tests/declared/oracle/called_in_ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/called_in_ghost.res.oracle
index 9d66c6a41ea..9957113d4d7 100644
--- a/src/plugins/variadic/tests/declared/oracle/called_in_ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/called_in_ghost.res.oracle
@@ -1,4 +1,4 @@
-[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
diff --git a/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle
index 77d342b3dd8..1a0792c2ff9 100644
--- a/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle
@@ -1,11 +1,10 @@
-[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
diff --git a/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle b/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle
index c028e9e151d..34cb2061442 100644
--- a/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle
@@ -1,10 +1,9 @@
-[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
diff --git a/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle
index f81ac2a39cf..c6a56c0319e 100644
--- a/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle
@@ -1,11 +1,10 @@
-[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
diff --git a/src/plugins/variadic/tests/declared/oracle/label.res.oracle b/src/plugins/variadic/tests/declared/oracle/label.res.oracle
index 427868a9c76..e4256555494 100644
--- a/src/plugins/variadic/tests/declared/oracle/label.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/label.res.oracle
@@ -1,10 +1,9 @@
-[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
diff --git a/src/plugins/variadic/tests/declared/oracle/multi.res.oracle b/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
index adcbb2b04d4..cb244196e32 100644
--- a/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
@@ -1,16 +1,14 @@
-[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
diff --git a/src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle
index 71fffe6ce34..abfb5632e9a 100644
--- a/src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle
@@ -1,7 +1,7 @@
[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
diff --git a/src/plugins/variadic/tests/declared/oracle/no-va.res.oracle b/src/plugins/variadic/tests/declared/oracle/no-va.res.oracle
index f00b72688a6..df9bae19b09 100644
--- a/src/plugins/variadic/tests/declared/oracle/no-va.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/no-va.res.oracle
@@ -1,7 +1,7 @@
[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
diff --git a/src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle
index 9dde9d6d2df..deaa01bb980 100644
--- a/src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle
@@ -1,11 +1,10 @@
-[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
diff --git a/src/plugins/variadic/tests/declared/oracle/rvalues.res.oracle b/src/plugins/variadic/tests/declared/oracle/rvalues.res.oracle
index 82863e34c74..9570cd50b5d 100644
--- a/src/plugins/variadic/tests/declared/oracle/rvalues.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/rvalues.res.oracle
@@ -1,10 +1,9 @@
-[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
diff --git a/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle
index fa2e63b8a11..f67021d13bf 100644
--- a/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle
@@ -1,11 +1,10 @@
-[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
diff --git a/src/plugins/variadic/tests/declared/oracle/simple.res.oracle b/src/plugins/variadic/tests/declared/oracle/simple.res.oracle
index 9112e947007..d605019696f 100644
--- a/src/plugins/variadic/tests/declared/oracle/simple.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/simple.res.oracle
@@ -1,10 +1,9 @@
-[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
diff --git a/src/plugins/variadic/tests/declared/oracle/struct.res.oracle b/src/plugins/variadic/tests/declared/oracle/struct.res.oracle
index 851c21816f4..2f716c490cd 100644
--- a/src/plugins/variadic/tests/declared/oracle/struct.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/struct.res.oracle
@@ -1,10 +1,9 @@
-[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
diff --git a/src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle
index 3038502c8de..94bbdbea2a1 100644
--- a/src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle
@@ -1,11 +1,11 @@
-[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
diff --git a/src/plugins/variadic/tests/declared/oracle/typedefed_function.res.oracle b/src/plugins/variadic/tests/declared/oracle/typedefed_function.res.oracle
index fa5cdfe98bb..f3795220e5d 100644
--- a/src/plugins/variadic/tests/declared/oracle/typedefed_function.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/typedefed_function.res.oracle
@@ -1,11 +1,10 @@
-[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
diff --git a/src/plugins/variadic/tests/defined/oracle/annot-formal.res.oracle b/src/plugins/variadic/tests/defined/oracle/annot-formal.res.oracle
index 208a9cae21b..5e9804ebfae 100644
--- a/src/plugins/variadic/tests/defined/oracle/annot-formal.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/annot-formal.res.oracle
@@ -1,6 +1,5 @@
-[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
diff --git a/src/plugins/variadic/tests/defined/oracle/annot-loc.res.oracle b/src/plugins/variadic/tests/defined/oracle/annot-loc.res.oracle
index 1a7b9cd9cf2..7a925bc77a1 100644
--- a/src/plugins/variadic/tests/defined/oracle/annot-loc.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/annot-loc.res.oracle
@@ -1,6 +1,5 @@
-[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
diff --git a/src/plugins/variadic/tests/defined/oracle/empty-vpar.res.oracle b/src/plugins/variadic/tests/defined/oracle/empty-vpar.res.oracle
index 7f338532acd..c908a44a049 100644
--- a/src/plugins/variadic/tests/defined/oracle/empty-vpar.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/empty-vpar.res.oracle
@@ -1,6 +1,5 @@
-[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
diff --git a/src/plugins/variadic/tests/defined/oracle/forward.res.oracle b/src/plugins/variadic/tests/defined/oracle/forward.res.oracle
index a7b3971db2a..1ad1f6de266 100644
--- a/src/plugins/variadic/tests/defined/oracle/forward.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/forward.res.oracle
@@ -1,6 +1,5 @@
-[variadic] tests/defined/forward.c:3: Declaration of variadic function sum.
-[variadic] tests/defined/forward.c:8:
- Generic translation of call to variadic function.
+[variadic] forward.c:3: Declaration of variadic function sum.
+[variadic] forward.c:8: Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/src/plugins/variadic/tests/defined/oracle/max.res.oracle b/src/plugins/variadic/tests/defined/oracle/max.res.oracle
index ded04c65a71..fdbc4879d71 100644
--- a/src/plugins/variadic/tests/defined/oracle/max.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/max.res.oracle
@@ -1,6 +1,5 @@
-[variadic] tests/defined/max.c:3: Declaration of variadic function max.
-[variadic] tests/defined/max.c:20:
- Generic translation of call to variadic function.
+[variadic] max.c:3: Declaration of variadic function max.
+[variadic] max.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
diff --git a/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle b/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle
index 7369a68d0b2..ed8db7e16c2 100644
--- a/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle
@@ -1,12 +1,10 @@
-[variadic] tests/defined/multiple-va_start.c:9:
- Declaration of variadic function pack.
-[variadic] tests/defined/multiple-va_start.c:32:
+[variadic] multiple-va_start.c:9: Declaration of variadic function pack.
+[variadic] multiple-va_start.c:32:
Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[eva] tests/defined/multiple-va_start.c:20:
- allocating variable __malloc_pack_l20
+[eva] multiple-va_start.c:20: allocating variable __malloc_pack_l20
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function pack:
diff --git a/src/plugins/variadic/tests/defined/oracle/pointers-to-va.res.oracle b/src/plugins/variadic/tests/defined/oracle/pointers-to-va.res.oracle
index 0bc3f144390..fcfbf225ed1 100644
--- a/src/plugins/variadic/tests/defined/oracle/pointers-to-va.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/pointers-to-va.res.oracle
@@ -1,13 +1,12 @@
-[variadic] tests/defined/pointers-to-va.c:6: Declaration of variadic function f.
-[variadic] tests/defined/pointers-to-va.c:17:
- Declaration of variadic function g.
-[variadic] tests/defined/pointers-to-va.c:31:
+[variadic] pointers-to-va.c:6: Declaration of variadic function f.
+[variadic] pointers-to-va.c:17: Declaration of variadic function g.
+[variadic] pointers-to-va.c:31:
Generic translation of call to variadic function.
-[variadic] tests/defined/pointers-to-va.c:32:
+[variadic] pointers-to-va.c:32:
Generic translation of call to variadic function.
-[variadic] tests/defined/pointers-to-va.c:33:
+[variadic] pointers-to-va.c:33:
Generic translation of call to variadic function.
-[variadic] tests/defined/pointers-to-va.c:34:
+[variadic] pointers-to-va.c:34:
Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
diff --git a/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle b/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle
index 9fcbfae2ed2..2fb73b23782 100644
--- a/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle
@@ -1,15 +1,12 @@
-[variadic] tests/defined/recursive.i:4: Declaration of variadic function f.
-[variadic] tests/defined/recursive.i:8:
- Generic translation of call to variadic function.
-[variadic] tests/defined/recursive.i:12:
- Generic translation of call to variadic function.
+[variadic] recursive.i:4: Declaration of variadic function f.
+[variadic] recursive.i:8: Generic translation of call to variadic function.
+[variadic] recursive.i:12: Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[eva] tests/defined/recursive.i:8: Warning:
- recursive call during value analysis
- of f (f <- f :: tests/defined/recursive.i:12 <- main). Assuming the call has
- no effect. The analysis will be unsound.
+[eva] recursive.i:8: Warning:
+ recursive call during value analysis of f (f <- f :: recursive.i:12 <- main).
+ Assuming the call has no effect. The analysis will be unsound.
[eva] using specification for function f
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/src/plugins/variadic/tests/defined/oracle/sentinel.res.oracle b/src/plugins/variadic/tests/defined/oracle/sentinel.res.oracle
index a2ee2ed266c..5d7fc79ffbb 100644
--- a/src/plugins/variadic/tests/defined/oracle/sentinel.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/sentinel.res.oracle
@@ -1,6 +1,5 @@
-[variadic] tests/defined/sentinel.c:3: Declaration of variadic function sum.
-[variadic] tests/defined/sentinel.c:21:
- Generic translation of call to variadic function.
+[variadic] sentinel.c:3: Declaration of variadic function sum.
+[variadic] sentinel.c:21: Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/src/plugins/variadic/tests/defined/oracle/simple.res.oracle b/src/plugins/variadic/tests/defined/oracle/simple.res.oracle
index 44c52cd1b73..66ca05b9798 100644
--- a/src/plugins/variadic/tests/defined/oracle/simple.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/simple.res.oracle
@@ -1,6 +1,5 @@
-[variadic] tests/defined/simple.c:4: Declaration of variadic function sum.
-[variadic] tests/defined/simple.c:19:
- Generic translation of call to variadic function.
+[variadic] simple.c:4: Declaration of variadic function sum.
+[variadic] simple.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
diff --git a/src/plugins/variadic/tests/defined/oracle/struct.res.oracle b/src/plugins/variadic/tests/defined/oracle/struct.res.oracle
index e65d36e637b..63a0918d464 100644
--- a/src/plugins/variadic/tests/defined/oracle/struct.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/struct.res.oracle
@@ -1,6 +1,5 @@
-[variadic] tests/defined/struct.c:18: Declaration of variadic function inter.
-[variadic] tests/defined/struct.c:41:
- Generic translation of call to variadic function.
+[variadic] struct.c:18: Declaration of variadic function inter.
+[variadic] struct.c:41: Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle b/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle
index 83a0ba4f9cf..9555e18f785 100644
--- a/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle
@@ -1,10 +1,9 @@
-[variadic] tests/defined/va_copy.c:9: Declaration of variadic function pack.
-[variadic] tests/defined/va_copy.c:32:
- Generic translation of call to variadic function.
+[variadic] va_copy.c:9: Declaration of variadic function pack.
+[variadic] va_copy.c:32: Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[eva] tests/defined/va_copy.c:21: allocating variable __malloc_pack_l21
+[eva] va_copy.c:21: allocating variable __malloc_pack_l21
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function pack:
diff --git a/src/plugins/variadic/tests/defined/oracle/va_list-as-arg.res.oracle b/src/plugins/variadic/tests/defined/oracle/va_list-as-arg.res.oracle
index 5fc590007e5..e60bb9ef10a 100644
--- a/src/plugins/variadic/tests/defined/oracle/va_list-as-arg.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/va_list-as-arg.res.oracle
@@ -1,6 +1,5 @@
-[variadic] tests/defined/va_list-as-arg.c:15:
- Declaration of variadic function sum.
-[variadic] tests/defined/va_list-as-arg.c:25:
+[variadic] va_list-as-arg.c:15: Declaration of variadic function sum.
+[variadic] va_list-as-arg.c:25:
Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
diff --git a/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle
index a1cffb94e46..d61d275a2e5 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/exec.res.oracle
@@ -4,19 +4,14 @@
Declaration of variadic function execle.
[variadic] FRAMAC_SHARE/libc/unistd.h:823:
Declaration of variadic function execlp.
-[variadic] tests/erroneous/exec.c:5: Warning:
+[variadic] exec.c:5: Warning:
Incorrect type for argument 3. The argument will be cast from int to char *.
-[variadic] tests/erroneous/exec.c:5:
- Translating call to execl to a call to execv.
-[variadic] tests/erroneous/exec.c:7: Warning:
+[variadic] exec.c:5: Translating call to execl to a call to execv.
+[variadic] exec.c:7: Warning:
Failed to find a sentinel (NULL pointer) in the argument list.
-[variadic] tests/erroneous/exec.c:7:
- Generic translation of call to variadic function.
-[variadic] tests/erroneous/exec.c:9: Warning:
- Not enough arguments: expected 5, given 4.
-[variadic] tests/erroneous/exec.c:9:
- Generic translation of call to variadic function.
-[variadic] tests/erroneous/exec.c:11: Warning:
+[variadic] exec.c:7: Generic translation of call to variadic function.
+[variadic] exec.c:9: Warning: Not enough arguments: expected 5, given 4.
+[variadic] exec.c:9: Generic translation of call to variadic function.
+[variadic] exec.c:11: Warning:
Incorrect type for argument 5. The argument will be cast from int to char * const *.
-[variadic] tests/erroneous/exec.c:11:
- Translating call to execle to a call to execve.
+[variadic] exec.c:11: Translating call to execle to a call to execve.
diff --git a/src/plugins/variadic/tests/erroneous/oracle/invalid_libc.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/invalid_libc.res.oracle
index 321767e5220..c830fa3b1f6 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/invalid_libc.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/invalid_libc.res.oracle
@@ -1,7 +1,5 @@
-[variadic] tests/erroneous/invalid_libc.i:2:
- Declaration of variadic function fprintf.
-[variadic] tests/erroneous/invalid_libc.i:2: Warning:
+[variadic] invalid_libc.i:2: Declaration of variadic function fprintf.
+[variadic] invalid_libc.i:2: Warning:
The standard function fprintf was expected to have at least 2 fixed parameters but only has 1.
No variadic translation will be performed.
-[variadic] tests/erroneous/invalid_libc.i:6:
- Generic translation of call to variadic function.
+[variadic] invalid_libc.i:6: Generic translation of call to variadic function.
diff --git a/src/plugins/variadic/tests/erroneous/oracle/no-libc.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/no-libc.res.oracle
index 64101cd01a7..6f2256ced84 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/no-libc.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/no-libc.res.oracle
@@ -1,5 +1,5 @@
-[variadic] tests/erroneous/no-libc.i:1: Declaration of variadic function printf.
+[variadic] no-libc.i:1: Declaration of variadic function printf.
[variadic] Warning: Unable to locate ACSL predicate valid_read_string which should be in the Frama-C LibC. Correct specifications can't be generated.
[variadic] Warning: Unable to locate global __fc_stdout which should be in the Frama-C LibC. Correct specifications can't be generated.
-[variadic] tests/erroneous/no-libc.i:5:
+[variadic] no-libc.i:5:
Translating call to printf to a call to the specialized version printf_va_1.
diff --git a/src/plugins/variadic/tests/erroneous/oracle/not-enough-par.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/not-enough-par.res.oracle
index c05a4ba9b29..74cb88e414f 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/not-enough-par.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/not-enough-par.res.oracle
@@ -1,4 +1,3 @@
-[kernel] tests/erroneous/not-enough-par.i:4: User Error:
- Too few arguments in call to f.
-[kernel] User Error: stopping on file "tests/erroneous/not-enough-par.i" that has errors.
+[kernel] not-enough-par.i:4: User Error: Too few arguments in call to f.
+[kernel] User Error: stopping on file "not-enough-par.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
index bf32832912e..b1fafb7e3bc 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/printf.res.oracle
@@ -14,8 +14,7 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:538:
Declaration of variadic function dprintf.
-[variadic] tests/erroneous/printf.c:8: Warning: Multiple usage of flag '-'.
-[variadic] tests/erroneous/printf.c:8: Warning:
+[variadic] printf.c:8: Warning: Multiple usage of flag '-'.
+[variadic] printf.c:8: Warning:
Flag ' ' and conversion specififer e are not compatibles.
-[variadic] tests/erroneous/printf.c:8:
- Generic translation of call to variadic function.
+[variadic] printf.c:8: Generic translation of call to variadic function.
diff --git a/src/plugins/variadic/tests/erroneous/oracle/va_arg-wrongtype.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/va_arg-wrongtype.res.oracle
index 63b857583a2..ff77e4725d8 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/va_arg-wrongtype.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/va_arg-wrongtype.res.oracle
@@ -1,6 +1,5 @@
-[variadic] tests/erroneous/va_arg-wrongtype.c:3:
- Declaration of variadic function sum.
-[variadic] tests/erroneous/va_arg-wrongtype.c:9: Warning:
+[variadic] va_arg-wrongtype.c:3: Declaration of variadic function sum.
+[variadic] va_arg-wrongtype.c:9: Warning:
Wrong type argument in va_start: short is promoted to int when used in the variadic part of the arguments. (You should pass int to va_start)
-[variadic] tests/erroneous/va_arg-wrongtype.c:18:
+[variadic] va_arg-wrongtype.c:18:
Generic translation of call to variadic function.
diff --git a/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle
index 7af1312eace..9688df149a0 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle
@@ -1,4 +1,4 @@
-[variadic] tests/erroneous/variadic-builtin.i:1:
+[variadic] variadic-builtin.i:1:
Variadic builtin Frama_C_show_each_warning left untransformed.
[kernel] Plug-in variadic aborted: unimplemented feature.
You may send a feature request at https://git.frama-c.com/pub/frama-c/issues with:
diff --git a/src/plugins/variadic/tests/erroneous/test_config b/src/plugins/variadic/tests/erroneous/test_config
index d42e13c1ae8..e5210fc9b6b 100644
--- a/src/plugins/variadic/tests/erroneous/test_config
+++ b/src/plugins/variadic/tests/erroneous/test_config
@@ -1 +1 @@
-OPT: -no-autoload-plugins -load-module variadic -check -kernel-verbose 0 -variadic-verbose 2
+OPT: -check -kernel-verbose 0 -variadic-verbose 2
diff --git a/src/plugins/variadic/tests/known/oracle/exec.res.oracle b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
index 956067e6dbe..496a4c83bbc 100644
--- a/src/plugins/variadic/tests/known/oracle/exec.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
@@ -4,22 +4,19 @@
Declaration of variadic function execle.
[variadic] FRAMAC_SHARE/libc/unistd.h:823:
Declaration of variadic function execlp.
-[variadic] tests/known/exec.c:9: Translating call to execle to a call to execve.
-[variadic] tests/known/exec.c:11: Warning:
+[variadic] exec.c:9: Translating call to execle to a call to execve.
+[variadic] exec.c:11: Warning:
Too many arguments: expected 5, given 6. Superfluous arguments will be removed.
-[variadic] tests/known/exec.c:11: Translating call to execl to a call to execv.
-[variadic] tests/known/exec.c:12: Warning:
+[variadic] exec.c:11: Translating call to execl to a call to execv.
+[variadic] exec.c:12: Warning:
Too many arguments: expected 4, given 5. Superfluous arguments will be removed.
-[variadic] tests/known/exec.c:12:
- Translating call to execlp to a call to execvp.
-[variadic] tests/known/exec.c:13: Warning:
+[variadic] exec.c:12: Translating call to execlp to a call to execvp.
+[variadic] exec.c:13: Warning:
Too many arguments: expected 4, given 6. Superfluous arguments will be removed.
-[variadic] tests/known/exec.c:13:
- Translating call to execle to a call to execve.
-[variadic] tests/known/exec.c:15: Warning:
+[variadic] exec.c:13: Translating call to execle to a call to execve.
+[variadic] exec.c:15: Warning:
Failed to find a sentinel (NULL pointer) in the argument list.
-[variadic] tests/known/exec.c:15:
- Generic translation of call to variadic function.
+[variadic] exec.c:15: Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/src/plugins/variadic/tests/known/oracle/exec_failed_requirement.res.oracle b/src/plugins/variadic/tests/known/oracle/exec_failed_requirement.res.oracle
index 47d6f5693dc..e7fb761c8dc 100644
--- a/src/plugins/variadic/tests/known/oracle/exec_failed_requirement.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/exec_failed_requirement.res.oracle
@@ -4,13 +4,13 @@
Declaration of variadic function execle.
[variadic] FRAMAC_SHARE/libc/unistd.h:823:
Declaration of variadic function execlp.
-[variadic] tests/known/exec_failed_requirement.c:7:
+[variadic] exec_failed_requirement.c:7:
Translating call to execl to a call to execv.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva] using specification for function execv
-[eva:alarm] tests/known/exec_failed_requirement.c:7: Warning:
+[eva:alarm] exec_failed_requirement.c:7: Warning:
function execv: precondition 'valid_string_argv0' got status invalid.
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle b/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
index 529a1b844f2..b2369bbf643 100644
--- a/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
@@ -3,13 +3,13 @@
[variadic] FRAMAC_SHARE/libc/fcntl.h:116: Declaration of variadic function open.
[variadic] FRAMAC_SHARE/libc/fcntl.h:122:
Declaration of variadic function openat.
-[variadic] tests/known/fcntl.c:8:
+[variadic] fcntl.c:8:
Translating call to the specialized version fcntl(int, int).
-[variadic] tests/known/fcntl.c:9:
+[variadic] fcntl.c:9:
Translating call to the specialized version fcntl(int, int, int).
-[variadic] tests/known/fcntl.c:10:
+[variadic] fcntl.c:10:
Translating call to the specialized version fcntl(int, int, struct flock *).
-[variadic] tests/known/fcntl.c:16: Warning:
+[variadic] fcntl.c:16: Warning:
No matching prototype found for this call to fcntl.
Expected candidates:
fcntl(int, int)
@@ -17,13 +17,12 @@
fcntl(int, int, struct flock *)
Given arguments:
fcntl(int, int, int, int)
-[variadic] tests/known/fcntl.c:16:
- Generic translation of call to variadic function.
-[variadic] tests/known/fcntl.c:20:
+[variadic] fcntl.c:16: Generic translation of call to variadic function.
+[variadic] fcntl.c:20:
Translating call to the specialized version fcntl(int, int).
-[variadic] tests/known/fcntl.c:24:
+[variadic] fcntl.c:24:
Translating call to the specialized version fcntl(int, int, struct flock *).
-[variadic] tests/known/fcntl.c:28: Warning:
+[variadic] fcntl.c:28: Warning:
No matching prototype found for this call to fcntl.
Expected candidates:
fcntl(int, int)
@@ -31,8 +30,7 @@
fcntl(int, int, struct flock *)
Given arguments:
fcntl(int, int, double)
-[variadic] tests/known/fcntl.c:28:
- Generic translation of call to variadic function.
+[variadic] fcntl.c:28: Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -40,9 +38,9 @@
[eva] using specification for function __va_fcntl_int
[eva] using specification for function __va_fcntl_flock
[eva] using specification for function fcntl
-[eva:alarm] tests/known/fcntl.c:20: Warning:
+[eva:alarm] fcntl.c:20: Warning:
function __va_fcntl_void: precondition 'cmd_has_void_arg' got status invalid.
-[eva:alarm] tests/known/fcntl.c:24: Warning:
+[eva:alarm] fcntl.c:24: Warning:
function __va_fcntl_flock: precondition 'cmd_as_flock_arg' got status invalid.
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/src/plugins/variadic/tests/known/oracle/ioctl.res.oracle b/src/plugins/variadic/tests/known/oracle/ioctl.res.oracle
index 195847c4a79..f7eb492e339 100644
--- a/src/plugins/variadic/tests/known/oracle/ioctl.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/ioctl.res.oracle
@@ -1,19 +1,19 @@
[variadic] FRAMAC_SHARE/libc/stropts.h:164:
Declaration of variadic function ioctl.
-[variadic] tests/known/ioctl.c:13:
+[variadic] ioctl.c:13:
Translating call to the specialized version ioctl(int, int).
-[variadic] tests/known/ioctl.c:15:
+[variadic] ioctl.c:15:
Translating call to the specialized version ioctl(int, int, void *).
-[variadic] tests/known/ioctl.c:17:
+[variadic] ioctl.c:17:
Translating call to the specialized version ioctl(int, int, void *).
-[variadic] tests/known/ioctl.c:18:
+[variadic] ioctl.c:18:
Translating call to the specialized version ioctl(int, int, int).
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva] using specification for function __va_ioctl_void
[eva] using specification for function __va_ioctl_ptr
-[eva:invalid-assigns] tests/known/ioctl.c:17:
+[eva:invalid-assigns] ioctl.c:17:
Completely invalid destination for assigns clause *((char *)argp + (0 ..)).
Ignoring.
[eva] using specification for function __va_ioctl_int
diff --git a/src/plugins/variadic/tests/known/oracle/open.res.oracle b/src/plugins/variadic/tests/known/oracle/open.res.oracle
index 840ef4ab762..0fcb6724a85 100644
--- a/src/plugins/variadic/tests/known/oracle/open.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/open.res.oracle
@@ -3,21 +3,20 @@
[variadic] FRAMAC_SHARE/libc/fcntl.h:116: Declaration of variadic function open.
[variadic] FRAMAC_SHARE/libc/fcntl.h:122:
Declaration of variadic function openat.
-[variadic] tests/known/open.c:7:
+[variadic] open.c:7:
Translating call to the specialized version open(char const *, int, mode_t).
-[variadic] tests/known/open.c:7: Warning:
+[variadic] open.c:7: Warning:
Incorrect type for argument 3. The argument will be cast from int to mode_t.
-[variadic] tests/known/open.c:8:
+[variadic] open.c:8:
Translating call to the specialized version open(char const *, int).
-[variadic] tests/known/open.c:9: Warning:
+[variadic] open.c:9: Warning:
No matching prototype found for this call to open.
Expected candidates:
open(char const *, int)
open(char const *, int, mode_t)
Given arguments:
open(char const *, int, int, int, char const *, int)
-[variadic] tests/known/open.c:9:
- Generic translation of call to variadic function.
+[variadic] open.c:9: Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle b/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
index b7200eb4eb8..eeb1928dbf3 100644
--- a/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
@@ -3,15 +3,14 @@
[variadic] FRAMAC_SHARE/libc/fcntl.h:116: Declaration of variadic function open.
[variadic] FRAMAC_SHARE/libc/fcntl.h:122:
Declaration of variadic function openat.
-[variadic] tests/known/open_wrong.c:13: Warning:
+[variadic] open_wrong.c:13: Warning:
No matching prototype found for this call to open.
Expected candidates:
open(char const *, int)
open(char const *, int, mode_t)
Given arguments:
open(char const *, int, char const *)
-[variadic] tests/known/open_wrong.c:13:
- Generic translation of call to variadic function.
+[variadic] open_wrong.c:13: Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/src/plugins/variadic/tests/known/oracle/openat.res.oracle b/src/plugins/variadic/tests/known/oracle/openat.res.oracle
index 045316f712a..daaa34b4a43 100644
--- a/src/plugins/variadic/tests/known/oracle/openat.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/openat.res.oracle
@@ -3,21 +3,20 @@
[variadic] FRAMAC_SHARE/libc/fcntl.h:116: Declaration of variadic function open.
[variadic] FRAMAC_SHARE/libc/fcntl.h:122:
Declaration of variadic function openat.
-[variadic] tests/known/openat.c:8:
+[variadic] openat.c:8:
Translating call to the specialized version openat(int, char const *, int, mode_t).
-[variadic] tests/known/openat.c:9:
+[variadic] openat.c:9:
Translating call to the specialized version openat(int, char const *, int, mode_t).
-[variadic] tests/known/openat.c:9: Warning:
+[variadic] openat.c:9: Warning:
Incorrect type for argument 4. The argument will be cast from int to mode_t.
-[variadic] tests/known/openat.c:10: Warning:
+[variadic] openat.c:10: Warning:
No matching prototype found for this call to openat.
Expected candidates:
openat(int, char const *, int)
openat(int, char const *, int, mode_t)
Given arguments:
openat(int, char const *, int, double)
-[variadic] tests/known/openat.c:10:
- Generic translation of call to variadic function.
+[variadic] openat.c:10: Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/src/plugins/variadic/tests/known/oracle/print_libc.res.oracle b/src/plugins/variadic/tests/known/oracle/print_libc.res.oracle
index fcce6d01157..ed919acd377 100644
--- a/src/plugins/variadic/tests/known/oracle/print_libc.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/print_libc.res.oracle
@@ -1,3 +1,3 @@
-[kernel] Parsing tests/known/print_libc.c (with preprocessing)
-[kernel] Parsing tests/known/empty.c (with preprocessing)
-[kernel] Parsing tests/known/result/print_libc.pretty.c (with preprocessing)
+[kernel] Parsing print_libc.c (with preprocessing)
+[kernel] Parsing empty.c (with preprocessing)
+[kernel] Parsing print_libc.pretty.c (with preprocessing)
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index d7102dda0aa..8d14fdb2e91 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -26,65 +26,64 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:538:
Declaration of variadic function dprintf.
-[variadic] tests/known/printf.c:37:
+[variadic] printf.c:37:
Translating call to printf to a call to the specialized version printf_va_1.
-[variadic] tests/known/printf.c:38:
+[variadic] printf.c:38:
Translating call to printf to a call to the specialized version printf_va_2.
-[variadic] tests/known/printf.c:39:
+[variadic] printf.c:39:
Translating call to printf to a call to the specialized version printf_va_3.
-[variadic] tests/known/printf.c:41:
+[variadic] printf.c:41:
Translating call to printf to a call to the specialized version printf_va_4.
-[variadic] tests/known/printf.c:42:
+[variadic] printf.c:42:
Translating call to printf to a call to the specialized version printf_va_5.
-[variadic] tests/known/printf.c:43:
+[variadic] printf.c:43:
Translating call to printf to a call to the specialized version printf_va_6.
-[variadic] tests/known/printf.c:44:
+[variadic] printf.c:44:
Translating call to printf to a call to the specialized version printf_va_7.
-[variadic] tests/known/printf.c:45:
+[variadic] printf.c:45:
Translating call to printf to a call to the specialized version printf_va_8.
-[variadic] tests/known/printf.c:46:
+[variadic] printf.c:46:
Translating call to printf to a call to the specialized version printf_va_9.
-[variadic] tests/known/printf.c:47:
+[variadic] printf.c:47:
Translating call to printf to a call to the specialized version printf_va_10.
-[variadic] tests/known/printf.c:48:
+[variadic] printf.c:48:
Translating call to printf to a call to the specialized version printf_va_11.
-[variadic] tests/known/printf.c:50:
+[variadic] printf.c:50:
Translating call to printf to a call to the specialized version printf_va_12.
-[variadic] tests/known/printf.c:51:
+[variadic] printf.c:51:
Translating call to printf to a call to the specialized version printf_va_13.
-[variadic] tests/known/printf.c:52:
+[variadic] printf.c:52:
Translating call to printf to a call to the specialized version printf_va_14.
-[variadic] tests/known/printf.c:53:
+[variadic] printf.c:53:
Translating call to printf to a call to the specialized version printf_va_15.
-[variadic] tests/known/printf.c:54:
+[variadic] printf.c:54:
Translating call to printf to a call to the specialized version printf_va_16.
-[variadic] tests/known/printf.c:55:
+[variadic] printf.c:55:
Translating call to printf to a call to the specialized version printf_va_17.
-[variadic] tests/known/printf.c:56:
+[variadic] printf.c:56:
Translating call to printf to a call to the specialized version printf_va_18.
-[variadic] tests/known/printf.c:58:
+[variadic] printf.c:58:
Translating call to printf to a call to the specialized version printf_va_19.
-[variadic] tests/known/printf.c:59:
+[variadic] printf.c:59:
Translating call to printf to a call to the specialized version printf_va_20.
-[variadic] tests/known/printf.c:60:
+[variadic] printf.c:60:
Translating call to printf to a call to the specialized version printf_va_21.
-[variadic] tests/known/printf.c:61:
+[variadic] printf.c:61:
Translating call to printf to a call to the specialized version printf_va_22.
-[variadic] tests/known/printf.c:63:
+[variadic] printf.c:63:
Translating call to printf to a call to the specialized version printf_va_23.
-[variadic] tests/known/printf.c:65:
+[variadic] printf.c:65:
Translating call to printf to a call to the specialized version printf_va_24.
-[variadic] tests/known/printf.c:68:
+[variadic] printf.c:68:
Translating call to printf to a call to the specialized version printf_va_25.
-[variadic] tests/known/printf.c:69:
+[variadic] printf.c:69:
Translating call to printf to a call to the specialized version printf_va_26.
-[variadic] tests/known/printf.c:71: Warning:
+[variadic] printf.c:71: Warning:
Flag ' ' and conversion specififer x are not compatibles.
-[variadic] tests/known/printf.c:71:
- Generic translation of call to variadic function.
-[variadic] tests/known/printf.c:74:
+[variadic] printf.c:71: Generic translation of call to variadic function.
+[variadic] printf.c:74:
Translating call to printf to a call to the specialized version printf_va_27.
-[variadic] tests/known/printf.c:75:
+[variadic] printf.c:75:
Translating call to printf to a call to the specialized version printf_va_28.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -115,7 +114,7 @@
[eva] using specification for function printf_va_24
[eva] using specification for function printf_va_25
[eva] using specification for function printf_va_26
-[kernel:annot:missing-spec] tests/known/printf.c:71: Warning:
+[kernel:annot:missing-spec] printf.c:71: Warning:
Neither code nor specification for function printf, generating default assigns from the prototype
[eva] using specification for function printf
[eva] using specification for function printf_va_27
diff --git a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
index e7591173023..e0bb8251627 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
@@ -14,21 +14,20 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:538:
Declaration of variadic function dprintf.
-[variadic] tests/known/printf_garbled_mix.c:8:
+[variadic] printf_garbled_mix.c:8:
Variadic builtin Frama_C_show_each_nb_printed left untransformed.
-[variadic] tests/known/printf_garbled_mix.c:7:
+[variadic] printf_garbled_mix.c:7:
Translating call to printf to a call to the specialized version printf_va_1.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[eva] tests/known/printf_garbled_mix.c:6:
+[eva] printf_garbled_mix.c:6:
Assigning imprecise value to b.
- The imprecision originates from Arithmetic
- {tests/known/printf_garbled_mix.c:6}
-[eva:alarm] tests/known/printf_garbled_mix.c:7: Warning:
+ The imprecision originates from Arithmetic {printf_garbled_mix.c:6}
+[eva:alarm] printf_garbled_mix.c:7: Warning:
pointer downcast. assert (unsigned int)b ≤ 2147483647;
[eva] using specification for function printf_va_1
-[eva] tests/known/printf_garbled_mix.c:8:
+[eva] printf_garbled_mix.c:8:
Frama_C_show_each_nb_printed: [-2147483648..2147483647]
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -40,8 +39,7 @@
S___fc_stdout[0].__fc_FILE_id ∈ [--..--]
[0].__fc_FILE_data ∈
{{ garbled mix of &{a}
- (origin: Library function
- {tests/known/printf_garbled_mix.c:7}) }}
+ (origin: Library function {printf_garbled_mix.c:7}) }}
[1] ∈ [--..--]
/* Generated by Frama-C */
#include "errno.h"
diff --git a/src/plugins/variadic/tests/known/oracle/printf_redefined.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_redefined.res.oracle
index 41b4f0c4fb8..a646cae3da3 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_redefined.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_redefined.res.oracle
@@ -1,10 +1,9 @@
-[variadic] tests/known/printf_redefined.i:3:
- Declaration of variadic function printf.
+[variadic] printf_redefined.i:3: Declaration of variadic function printf.
[variadic] Warning: Unable to locate ACSL predicate valid_read_string which should be in the Frama-C LibC. Correct specifications can't be generated.
[variadic] Warning: Unable to locate global __fc_stdout which should be in the Frama-C LibC. Correct specifications can't be generated.
-[variadic] tests/known/printf_redefined.i:7:
+[variadic] printf_redefined.i:7:
Translating call to printf to a call to the specialized version printf_va_1.
-[variadic] tests/known/printf_redefined.i:7: Warning:
+[variadic] printf_redefined.i:7: Warning:
Incorrect type for argument 2. The argument will be cast from long to size_t.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
index 4ee27be4661..804a65eac3d 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
@@ -14,21 +14,21 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:538:
Declaration of variadic function dprintf.
-[variadic] tests/known/printf_wrong_arity.c:8:
+[variadic] printf_wrong_arity.c:8:
Translating call to printf to a call to the specialized version printf_va_1.
-[variadic] tests/known/printf_wrong_arity.c:8: Warning:
+[variadic] printf_wrong_arity.c:8: Warning:
Too many arguments: expected 2, given 3. Superfluous arguments will be removed.
-[variadic] tests/known/printf_wrong_arity.c:9:
+[variadic] printf_wrong_arity.c:9:
Translating call to printf to a call to the specialized version printf_va_2.
-[variadic] tests/known/printf_wrong_arity.c:9: Warning:
+[variadic] printf_wrong_arity.c:9: Warning:
Not enough arguments: expected 3, given 2.
-[variadic] tests/known/printf_wrong_arity.c:9:
+[variadic] printf_wrong_arity.c:9:
Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva] using specification for function printf_va_1
-[kernel:annot:missing-spec] tests/known/printf_wrong_arity.c:9: Warning:
+[kernel:annot:missing-spec] printf_wrong_arity.c:9: Warning:
Neither code nor specification for function printf, generating default assigns from the prototype
[eva] using specification for function printf
[eva] done for function main
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
index 2c72bbbab04..e7020976a8b 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle
@@ -14,29 +14,29 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:538:
Declaration of variadic function dprintf.
-[variadic] tests/known/printf_wrong_pointers.c:14:
+[variadic] printf_wrong_pointers.c:14:
Translating call to printf to a call to the specialized version printf_va_1.
-[variadic] tests/known/printf_wrong_pointers.c:15:
+[variadic] printf_wrong_pointers.c:15:
Translating call to printf to a call to the specialized version printf_va_2.
-[variadic] tests/known/printf_wrong_pointers.c:16:
+[variadic] printf_wrong_pointers.c:16:
Translating call to printf to a call to the specialized version printf_va_3.
-[variadic] tests/known/printf_wrong_pointers.c:17:
+[variadic] printf_wrong_pointers.c:17:
Translating call to printf to a call to the specialized version printf_va_4.
-[variadic] tests/known/printf_wrong_pointers.c:18:
+[variadic] printf_wrong_pointers.c:18:
Translating call to printf to a call to the specialized version printf_va_5.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva] using specification for function printf_va_1
-[eva:alarm] tests/known/printf_wrong_pointers.c:14: Warning:
+[eva:alarm] printf_wrong_pointers.c:14: Warning:
function printf_va_1: precondition \valid(param0) got status invalid.
[eva] using specification for function printf_va_2
[eva] using specification for function printf_va_3
-[eva:alarm] tests/known/printf_wrong_pointers.c:16: Warning:
+[eva:alarm] printf_wrong_pointers.c:16: Warning:
function printf_va_3: precondition \valid(param0) got status invalid.
[eva] using specification for function printf_va_4
[eva] using specification for function printf_va_5
-[eva:alarm] tests/known/printf_wrong_pointers.c:18: Warning:
+[eva:alarm] printf_wrong_pointers.c:18: Warning:
function printf_va_5: precondition valid_read_wstring(param0) got status invalid.
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
index 5d41306e7d7..e523ee334bc 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
@@ -14,65 +14,65 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:538:
Declaration of variadic function dprintf.
-[variadic] tests/known/printf_wrong_types.c:18:
+[variadic] printf_wrong_types.c:18:
Translating call to printf to a call to the specialized version printf_va_1.
-[variadic] tests/known/printf_wrong_types.c:19:
+[variadic] printf_wrong_types.c:19:
Translating call to printf to a call to the specialized version printf_va_2.
-[variadic] tests/known/printf_wrong_types.c:19: Warning:
+[variadic] printf_wrong_types.c:19: Warning:
Incorrect type for argument 2. The argument will be cast from unsigned int to int.
-[variadic] tests/known/printf_wrong_types.c:20:
+[variadic] printf_wrong_types.c:20:
Translating call to printf to a call to the specialized version printf_va_3.
-[variadic] tests/known/printf_wrong_types.c:20: Warning:
+[variadic] printf_wrong_types.c:20: Warning:
Incorrect type for argument 2. The argument will be cast from int to unsigned int.
-[variadic] tests/known/printf_wrong_types.c:21:
+[variadic] printf_wrong_types.c:21:
Translating call to printf to a call to the specialized version printf_va_4.
-[variadic] tests/known/printf_wrong_types.c:21: Warning:
+[variadic] printf_wrong_types.c:21: Warning:
Incorrect type for argument 2. The argument will be cast from int to long.
-[variadic] tests/known/printf_wrong_types.c:22:
+[variadic] printf_wrong_types.c:22:
Translating call to printf to a call to the specialized version printf_va_5.
-[variadic] tests/known/printf_wrong_types.c:22: Warning:
+[variadic] printf_wrong_types.c:22: Warning:
Incorrect type for argument 2. The argument will be cast from long to int.
-[variadic] tests/known/printf_wrong_types.c:23:
+[variadic] printf_wrong_types.c:23:
Translating call to printf to a call to the specialized version printf_va_6.
-[variadic] tests/known/printf_wrong_types.c:23: Warning:
+[variadic] printf_wrong_types.c:23: Warning:
Incorrect type for argument 2. The argument will be cast from unsigned int to unsigned long.
-[variadic] tests/known/printf_wrong_types.c:24:
+[variadic] printf_wrong_types.c:24:
Translating call to printf to a call to the specialized version printf_va_7.
-[variadic] tests/known/printf_wrong_types.c:24: Warning:
+[variadic] printf_wrong_types.c:24: Warning:
Incorrect type for argument 2. The argument will be cast from unsigned long to unsigned int.
-[variadic] tests/known/printf_wrong_types.c:25:
+[variadic] printf_wrong_types.c:25:
Translating call to printf to a call to the specialized version printf_va_8.
-[variadic] tests/known/printf_wrong_types.c:25: Warning:
+[variadic] printf_wrong_types.c:25: Warning:
Incorrect type for argument 2. The argument will be cast from unsigned int to void *.
-[variadic] tests/known/printf_wrong_types.c:26:
+[variadic] printf_wrong_types.c:26:
Translating call to printf to a call to the specialized version printf_va_9.
-[variadic] tests/known/printf_wrong_types.c:27:
+[variadic] printf_wrong_types.c:27:
Translating call to printf to a call to the specialized version printf_va_10.
-[variadic] tests/known/printf_wrong_types.c:27: Warning:
+[variadic] printf_wrong_types.c:27: Warning:
Incorrect type for argument 2. The argument will be cast from long double to double.
-[variadic] tests/known/printf_wrong_types.c:28:
+[variadic] printf_wrong_types.c:28:
Translating call to printf to a call to the specialized version printf_va_11.
-[variadic] tests/known/printf_wrong_types.c:28: Warning:
+[variadic] printf_wrong_types.c:28: Warning:
Incorrect type for argument 2. The argument will be cast from long double to double.
-[variadic] tests/known/printf_wrong_types.c:29:
+[variadic] printf_wrong_types.c:29:
Translating call to printf to a call to the specialized version printf_va_12.
-[variadic] tests/known/printf_wrong_types.c:29: Warning:
+[variadic] printf_wrong_types.c:29: Warning:
Incorrect type for argument 2. The argument will be cast from double to long double.
-[variadic] tests/known/printf_wrong_types.c:30:
+[variadic] printf_wrong_types.c:30:
Translating call to printf to a call to the specialized version printf_va_13.
-[variadic] tests/known/printf_wrong_types.c:30: Warning:
+[variadic] printf_wrong_types.c:30: Warning:
Incorrect type for argument 2. The argument will be cast from int to char *.
-[variadic] tests/known/printf_wrong_types.c:31:
+[variadic] printf_wrong_types.c:31:
Translating call to printf to a call to the specialized version printf_va_14.
-[variadic] tests/known/printf_wrong_types.c:31: Warning:
+[variadic] printf_wrong_types.c:31: Warning:
Incorrect type for argument 2. The argument will be cast from char * to int.
-[variadic] tests/known/printf_wrong_types.c:35:
+[variadic] printf_wrong_types.c:35:
Translating call to printf to a call to the specialized version printf_va_15.
-[variadic] tests/known/printf_wrong_types.c:35: Warning:
+[variadic] printf_wrong_types.c:35: Warning:
Possible portability issues with enum type for argument 2 (use -variadic-no-strict to avoid this warning).
-[variadic] tests/known/printf_wrong_types.c:36:
+[variadic] printf_wrong_types.c:36:
Translating call to printf to a call to the specialized version printf_va_16.
-[variadic] tests/known/printf_wrong_types.c:36: Warning:
+[variadic] printf_wrong_types.c:36: Warning:
Incorrect type for argument 2. The argument will be cast from RC (unsigned int) to int.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -90,7 +90,7 @@
[eva] using specification for function printf_va_11
[eva] using specification for function printf_va_12
[eva] using specification for function printf_va_13
-[eva:alarm] tests/known/printf_wrong_types.c:30: Warning:
+[eva:alarm] printf_wrong_types.c:30: Warning:
function printf_va_13: precondition valid_read_string(param0) got status invalid.
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -351,7 +351,7 @@ int main(void)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[kernel:annot:missing-spec] tests/known/printf_wrong_types.c:18: Warning:
+[kernel:annot:missing-spec] printf_wrong_types.c:18: Warning:
Neither code nor specification for function printf, generating default assigns from the prototype
[eva] using specification for function printf
[eva] done for function main
@@ -426,55 +426,55 @@ int main(void)
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:538:
Declaration of variadic function dprintf.
-[variadic] tests/known/printf_wrong_types.c:18:
+[variadic] printf_wrong_types.c:18:
Translating call to printf to a call to the specialized version printf_va_1.
-[variadic] tests/known/printf_wrong_types.c:19:
+[variadic] printf_wrong_types.c:19:
Translating call to printf to a call to the specialized version printf_va_2.
-[variadic] tests/known/printf_wrong_types.c:19: Warning:
+[variadic] printf_wrong_types.c:19: Warning:
Incorrect type for argument 2. The argument will be cast from unsigned int to int.
-[variadic] tests/known/printf_wrong_types.c:20:
+[variadic] printf_wrong_types.c:20:
Translating call to printf to a call to the specialized version printf_va_3.
-[variadic] tests/known/printf_wrong_types.c:20: Warning:
+[variadic] printf_wrong_types.c:20: Warning:
Incorrect type for argument 2. The argument will be cast from int to unsigned int.
-[variadic] tests/known/printf_wrong_types.c:21:
+[variadic] printf_wrong_types.c:21:
Translating call to printf to a call to the specialized version printf_va_4.
-[variadic] tests/known/printf_wrong_types.c:22:
+[variadic] printf_wrong_types.c:22:
Translating call to printf to a call to the specialized version printf_va_5.
-[variadic] tests/known/printf_wrong_types.c:23:
+[variadic] printf_wrong_types.c:23:
Translating call to printf to a call to the specialized version printf_va_6.
-[variadic] tests/known/printf_wrong_types.c:24:
+[variadic] printf_wrong_types.c:24:
Translating call to printf to a call to the specialized version printf_va_7.
-[variadic] tests/known/printf_wrong_types.c:25:
+[variadic] printf_wrong_types.c:25:
Translating call to printf to a call to the specialized version printf_va_8.
-[variadic] tests/known/printf_wrong_types.c:25: Warning:
+[variadic] printf_wrong_types.c:25: Warning:
Incorrect type for argument 2. The argument will be cast from unsigned int to void *.
-[variadic] tests/known/printf_wrong_types.c:26:
+[variadic] printf_wrong_types.c:26:
Translating call to printf to a call to the specialized version printf_va_9.
-[variadic] tests/known/printf_wrong_types.c:27:
+[variadic] printf_wrong_types.c:27:
Translating call to printf to a call to the specialized version printf_va_10.
-[variadic] tests/known/printf_wrong_types.c:27: Warning:
+[variadic] printf_wrong_types.c:27: Warning:
Incorrect type for argument 2. The argument will be cast from long double to double.
-[variadic] tests/known/printf_wrong_types.c:28:
+[variadic] printf_wrong_types.c:28:
Translating call to printf to a call to the specialized version printf_va_11.
-[variadic] tests/known/printf_wrong_types.c:28: Warning:
+[variadic] printf_wrong_types.c:28: Warning:
Incorrect type for argument 2. The argument will be cast from long double to double.
-[variadic] tests/known/printf_wrong_types.c:29:
+[variadic] printf_wrong_types.c:29:
Translating call to printf to a call to the specialized version printf_va_12.
-[variadic] tests/known/printf_wrong_types.c:29: Warning:
+[variadic] printf_wrong_types.c:29: Warning:
Incorrect type for argument 2. The argument will be cast from double to long double.
-[variadic] tests/known/printf_wrong_types.c:30:
+[variadic] printf_wrong_types.c:30:
Translating call to printf to a call to the specialized version printf_va_13.
-[variadic] tests/known/printf_wrong_types.c:30: Warning:
+[variadic] printf_wrong_types.c:30: Warning:
Incorrect type for argument 2. The argument will be cast from int to char *.
-[variadic] tests/known/printf_wrong_types.c:31:
+[variadic] printf_wrong_types.c:31:
Translating call to printf to a call to the specialized version printf_va_14.
-[variadic] tests/known/printf_wrong_types.c:31: Warning:
+[variadic] printf_wrong_types.c:31: Warning:
Incorrect type for argument 2. The argument will be cast from char * to int.
-[variadic] tests/known/printf_wrong_types.c:35:
+[variadic] printf_wrong_types.c:35:
Translating call to printf to a call to the specialized version printf_va_15.
-[variadic] tests/known/printf_wrong_types.c:36:
+[variadic] printf_wrong_types.c:36:
Translating call to printf to a call to the specialized version printf_va_16.
-[variadic] tests/known/printf_wrong_types.c:36: Warning:
+[variadic] printf_wrong_types.c:36: Warning:
Incorrect type for argument 2. The argument will be cast from RC (unsigned int) to int.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -492,7 +492,7 @@ int main(void)
[eva] using specification for function printf_va_11
[eva] using specification for function printf_va_12
[eva] using specification for function printf_va_13
-[eva:alarm] tests/known/printf_wrong_types.c:30: Warning:
+[eva:alarm] printf_wrong_types.c:30: Warning:
function printf_va_13: precondition valid_read_string(param0) got status invalid.
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/src/plugins/variadic/tests/known/oracle/scanf.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
index bf4a9d81548..af4cc6e94af 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf.res.oracle
@@ -14,7 +14,7 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:538:
Declaration of variadic function dprintf.
-[variadic] tests/known/scanf.c:7:
+[variadic] scanf.c:7:
Translating call to scanf to a call to the specialized version scanf_va_1.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
diff --git a/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
index e563ba2f274..fa1b0a80a48 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf_loop.res.oracle
@@ -14,7 +14,7 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:538:
Declaration of variadic function dprintf.
-[variadic] tests/known/scanf_loop.c:6:
+[variadic] scanf_loop.c:6:
Translating call to scanf to a call to the specialized version scanf_va_1.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
diff --git a/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle b/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
index 704b3de7532..7ecea7ad0fc 100644
--- a/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/scanf_wrong.res.oracle
@@ -14,18 +14,17 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:538:
Declaration of variadic function dprintf.
-[variadic] tests/known/scanf_wrong.c:8:
+[variadic] scanf_wrong.c:8:
Translating call to scanf to a call to the specialized version scanf_va_1.
-[variadic] tests/known/scanf_wrong.c:8: Warning:
+[variadic] scanf_wrong.c:8: Warning:
Incorrect type for argument 2. The argument will be cast from double to char *.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[eva:alarm] tests/known/scanf_wrong.c:8: Warning:
+[eva:alarm] scanf_wrong.c:8: Warning:
accessing uninitialized left-value. assert \initialized(&d);
[eva] done for function main
-[eva] tests/known/scanf_wrong.c:8:
- assertion 'Eva,initialization' got final status invalid.
+[eva] scanf_wrong.c:8: assertion 'Eva,initialization' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
NON TERMINATING FUNCTION
diff --git a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
index cecc5cc5431..e51a5c3ce8a 100644
--- a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
@@ -14,9 +14,9 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:538:
Declaration of variadic function dprintf.
-[variadic] tests/known/snprintf.c:12:
+[variadic] snprintf.c:12:
Translating call to snprintf to a call to the specialized version snprintf_va_1.
-[variadic] tests/known/snprintf.c:15:
+[variadic] snprintf.c:15:
Translating call to snprintf to a call to the specialized version snprintf_va_2.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -24,14 +24,14 @@
[eva] FRAMAC_SHARE/libc/string.h:118:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
[eva] using specification for function snprintf_va_1
-[eva] tests/known/snprintf.c:12:
+[eva] snprintf.c:12:
Cannot evaluate range bound format_length(format) - 1
(unsupported ACSL construct: logic function format_length). Approximating
-[eva:alarm] tests/known/snprintf.c:12: Warning:
+[eva:alarm] snprintf.c:12: Warning:
function snprintf_va_1: precondition \valid(s + (0 .. n - 1)) ∨
\valid(s +
(0 .. format_length(format) - 1)) got status unknown.
-[eva:alarm] tests/known/snprintf.c:13: Warning:
+[eva:alarm] snprintf.c:13: Warning:
assertion got status invalid (stopping propagation).
[eva] using specification for function snprintf_va_2
[eva] done for function main
diff --git a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
index cc3c40be6d6..2465387928b 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
@@ -14,50 +14,44 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:538:
Declaration of variadic function dprintf.
-[variadic] tests/known/stdio_print.c:9: Warning:
+[variadic] stdio_print.c:9: Warning:
Call to function fprintf with non-static format argument:
no specification will be generated.
-[variadic] tests/known/stdio_print.c:9:
- Generic translation of call to variadic function.
-[variadic] tests/known/stdio_print.c:10: Warning:
+[variadic] stdio_print.c:9: Generic translation of call to variadic function.
+[variadic] stdio_print.c:10: Warning:
Call to function printf with non-static format argument:
no specification will be generated.
-[variadic] tests/known/stdio_print.c:10:
- Generic translation of call to variadic function.
-[variadic] tests/known/stdio_print.c:11: Warning:
+[variadic] stdio_print.c:10: Generic translation of call to variadic function.
+[variadic] stdio_print.c:11: Warning:
Call to function snprintf with non-static format argument:
no specification will be generated.
-[variadic] tests/known/stdio_print.c:11:
- Generic translation of call to variadic function.
-[variadic] tests/known/stdio_print.c:12: Warning:
+[variadic] stdio_print.c:11: Generic translation of call to variadic function.
+[variadic] stdio_print.c:12: Warning:
Call to function sprintf with non-static format argument:
no specification will be generated.
-[variadic] tests/known/stdio_print.c:12:
- Generic translation of call to variadic function.
-[variadic] tests/known/stdio_print.c:13: Warning:
+[variadic] stdio_print.c:12: Generic translation of call to variadic function.
+[variadic] stdio_print.c:13: Warning:
Call to function dprintf with non-static format argument:
no specification will be generated.
-[variadic] tests/known/stdio_print.c:13:
- Generic translation of call to variadic function.
-[variadic] tests/known/stdio_print.c:15:
+[variadic] stdio_print.c:13: Generic translation of call to variadic function.
+[variadic] stdio_print.c:15:
Translating call to fprintf to a call to the specialized version fprintf_va_1.
-[variadic] tests/known/stdio_print.c:16:
+[variadic] stdio_print.c:16:
Translating call to printf to a call to the specialized version printf_va_1.
-[variadic] tests/known/stdio_print.c:17:
+[variadic] stdio_print.c:17:
Translating call to snprintf to a call to the specialized version snprintf_va_1.
-[variadic] tests/known/stdio_print.c:18:
+[variadic] stdio_print.c:18:
Translating call to sprintf to a call to the specialized version sprintf_va_1.
-[variadic] tests/known/stdio_print.c:19:
+[variadic] stdio_print.c:19:
Translating call to dprintf to a call to the specialized version dprintf_va_1.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[eva:alarm] tests/known/stdio_print.c:9: Warning:
+[eva:alarm] stdio_print.c:9: Warning:
accessing uninitialized left-value. assert \initialized(&format);
[eva] done for function main
-[eva] tests/known/stdio_print.c:9:
- assertion 'Eva,initialization' got final status invalid.
-[kernel:annot:missing-spec] tests/known/stdio_print.c:9: Warning:
+[eva] stdio_print.c:9: assertion 'Eva,initialization' got final status invalid.
+[kernel:annot:missing-spec] stdio_print.c:9: Warning:
Neither code nor specification for function fprintf, generating default assigns from the prototype
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
diff --git a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
index f157c9d36bf..21d76e6c0ea 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
@@ -14,35 +14,31 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:538:
Declaration of variadic function dprintf.
-[variadic] tests/known/stdio_scan.c:10: Warning:
+[variadic] stdio_scan.c:10: Warning:
Call to function fscanf with non-static format argument:
no specification will be generated.
-[variadic] tests/known/stdio_scan.c:10:
- Generic translation of call to variadic function.
-[variadic] tests/known/stdio_scan.c:11: Warning:
+[variadic] stdio_scan.c:10: Generic translation of call to variadic function.
+[variadic] stdio_scan.c:11: Warning:
Call to function scanf with non-static format argument:
no specification will be generated.
-[variadic] tests/known/stdio_scan.c:11:
- Generic translation of call to variadic function.
-[variadic] tests/known/stdio_scan.c:12: Warning:
+[variadic] stdio_scan.c:11: Generic translation of call to variadic function.
+[variadic] stdio_scan.c:12: Warning:
Call to function sscanf with non-static format argument:
no specification will be generated.
-[variadic] tests/known/stdio_scan.c:12:
- Generic translation of call to variadic function.
-[variadic] tests/known/stdio_scan.c:14:
+[variadic] stdio_scan.c:12: Generic translation of call to variadic function.
+[variadic] stdio_scan.c:14:
Translating call to fscanf to a call to the specialized version fscanf_va_1.
-[variadic] tests/known/stdio_scan.c:15:
+[variadic] stdio_scan.c:15:
Translating call to scanf to a call to the specialized version scanf_va_1.
-[variadic] tests/known/stdio_scan.c:16:
+[variadic] stdio_scan.c:16:
Translating call to sscanf to a call to the specialized version sscanf_va_1.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[eva:alarm] tests/known/stdio_scan.c:10: Warning:
+[eva:alarm] stdio_scan.c:10: Warning:
accessing uninitialized left-value. assert \initialized(&s);
[eva] done for function main
-[eva] tests/known/stdio_scan.c:10:
- assertion 'Eva,initialization' got final status invalid.
+[eva] stdio_scan.c:10: assertion 'Eva,initialization' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
NON TERMINATING FUNCTION
diff --git a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
index 585983473b2..5fa13ac427e 100644
--- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
@@ -26,23 +26,23 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:538:
Declaration of variadic function dprintf.
-[variadic] tests/known/swprintf.c:12:
+[variadic] swprintf.c:12:
Translating call to swprintf to a call to the specialized version swprintf_va_1.
-[variadic] tests/known/swprintf.c:15:
+[variadic] swprintf.c:15:
Translating call to swprintf to a call to the specialized version swprintf_va_2.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva] using specification for function wmemset
[eva] using specification for function swprintf_va_1
-[eva] tests/known/swprintf.c:12:
+[eva] swprintf.c:12:
Cannot evaluate range bound wformat_length(format) - 1
(unsupported ACSL construct: logic function wformat_length). Approximating
-[eva:alarm] tests/known/swprintf.c:12: Warning:
+[eva:alarm] swprintf.c:12: Warning:
function swprintf_va_1: precondition \valid(ws + (0 .. n - 1)) ∨
\valid(ws +
(0 .. wformat_length(format) - 1)) got status unknown.
-[eva:alarm] tests/known/swprintf.c:13: Warning:
+[eva:alarm] swprintf.c:13: Warning:
assertion got status invalid (stopping propagation).
[eva] using specification for function swprintf_va_2
[eva] done for function main
diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
index b85bb1c1d06..11cacf32ca2 100644
--- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
@@ -26,25 +26,25 @@
Declaration of variadic function sscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:538:
Declaration of variadic function dprintf.
-[variadic] tests/known/wchar.c:11:
+[variadic] wchar.c:11:
Translating call to wprintf to a call to the specialized version wprintf_va_1.
-[variadic] tests/known/wchar.c:12:
+[variadic] wchar.c:12:
Translating call to wprintf to a call to the specialized version wprintf_va_2.
-[variadic] tests/known/wchar.c:13:
+[variadic] wchar.c:13:
Translating call to wprintf to a call to the specialized version wprintf_va_3.
-[variadic] tests/known/wchar.c:14:
+[variadic] wchar.c:14:
Translating call to wprintf to a call to the specialized version wprintf_va_4.
-[variadic] tests/known/wchar.c:15:
+[variadic] wchar.c:15:
Translating call to wprintf to a call to the specialized version wprintf_va_5.
-[variadic] tests/known/wchar.c:16:
+[variadic] wchar.c:16:
Translating call to wprintf to a call to the specialized version wprintf_va_6.
-[variadic] tests/known/wchar.c:18:
+[variadic] wchar.c:18:
Translating call to swprintf to a call to the specialized version swprintf_va_1.
-[variadic] tests/known/wchar.c:20:
+[variadic] wchar.c:20:
Translating call to wscanf to a call to the specialized version wscanf_va_1.
-[variadic] tests/known/wchar.c:21:
+[variadic] wchar.c:21:
Translating call to wscanf to a call to the specialized version wscanf_va_2.
-[variadic] tests/known/wchar.c:23:
+[variadic] wchar.c:23:
Translating call to swscanf to a call to the specialized version swscanf_va_1.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
diff --git a/src/plugins/variadic/tests/known/print_libc.c b/src/plugins/variadic/tests/known/print_libc.c
index 265018f2c74..db33468ad75 100644
--- a/src/plugins/variadic/tests/known/print_libc.c
+++ b/src/plugins/variadic/tests/known/print_libc.c
@@ -1,6 +1,6 @@
/* run.config
LOG: print_libc.pretty.c
- OPT: @PTEST_DIR@/empty.c -no-autoload-plugins -load-module variadic -no-print-libc -print -ocode @PTEST_DIR@/result/@PTEST_NAME@.pretty.c -then @PTEST_DIR@/result/@PTEST_NAME@.pretty.c
+ OPT: %{dep:empty.c} -no-print-libc -print -ocode @PTEST_NAME@.pretty.c -then @PTEST_NAME@.pretty.c
*/
#include <stdio.h>
diff --git a/src/plugins/variadic/tests/ptests_config b/src/plugins/variadic/tests/ptests_config
new file mode 100644
index 00000000000..6fa0daf0fa1
--- /dev/null
+++ b/src/plugins/variadic/tests/ptests_config
@@ -0,0 +1 @@
+DEFAULT_SUITES= declared defined erroneous known
diff --git a/src/plugins/variadic/tests/test_config b/src/plugins/variadic/tests/test_config
index e076935b234..3a9dd329444 100644
--- a/src/plugins/variadic/tests/test_config
+++ b/src/plugins/variadic/tests/test_config
@@ -1 +1,2 @@
-OPT: -no-autoload-plugins -load-module from,inout,eva,variadic,scope -check -print -kernel-verbose 0 -variadic-verbose 2 -eva -eva-slevel 10 -eva-msg-key=-initial-state,-summary -eva-no-show-progress -eva-print
+PLUGIN: from inout eva variadic scope
+OPT: -check -print -kernel-verbose 0 -variadic-verbose 2 -eva -eva-slevel 10 -eva-msg-key=-initial-state,-summary -eva-no-show-progress -eva-print
--
GitLab