From 1b807716385f9ab8ebc7273bf5f8bed9bbfad276 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 3 Oct 2019 18:34:41 +0200
Subject: [PATCH] [Variadic] Moves .c tests into .i when possible
---
...pty-vpar-with-ghost.c => empty-vpar-with-ghost.i} | 0
.../tests/declared/{empty-vpar.c => empty-vpar.i} | 0
...on-ptr-with-ghost.c => function-ptr-with-ghost.i} | 0
.../variadic/tests/declared/{label.c => label.i} | 0
.../variadic/tests/declared/{multi.c => multi.i} | 0
.../{no-va-with-ghost.c => no-va-with-ghost.i} | 0
.../variadic/tests/declared/{no-va.c => no-va.i} | 0
.../declared/oracle/empty-vpar-with-ghost.res.oracle | 6 +++---
.../tests/declared/oracle/empty-vpar.res.oracle | 6 +++---
.../oracle/function-ptr-with-ghost.res.oracle | 6 +++---
.../variadic/tests/declared/oracle/label.res.oracle | 6 +++---
.../variadic/tests/declared/oracle/multi.res.oracle | 12 ++++++------
.../declared/oracle/no-va-with-ghost.res.oracle | 2 +-
.../variadic/tests/declared/oracle/no-va.res.oracle | 2 +-
.../declared/oracle/rvalues-with-ghost.res.oracle | 6 +++---
.../tests/declared/oracle/rvalues.res.oracle | 6 +++---
.../declared/oracle/simple-with-ghost.res.oracle | 6 +++---
.../variadic/tests/declared/oracle/simple.res.oracle | 6 +++---
.../variadic/tests/declared/oracle/struct.res.oracle | 6 +++---
.../oracle/typedefed_function-with-ghost.res.oracle | 6 +++---
.../declared/oracle/typedefed_function.res.oracle | 6 +++---
.../{rvalues-with-ghost.c => rvalues-with-ghost.i} | 0
.../variadic/tests/declared/{rvalues.c => rvalues.i} | 0
.../{simple-with-ghost.c => simple-with-ghost.i} | 0
.../variadic/tests/declared/{simple.c => simple.i} | 0
.../variadic/tests/declared/{struct.c => struct.i} | 0
...-with-ghost.c => typedefed_function-with-ghost.i} | 0
.../{typedefed_function.c => typedefed_function.i} | 0
.../tests/defined/oracle/recursive.res.oracle | 10 +++++-----
.../tests/defined/{recursive.c => recursive.i} | 0
.../erroneous/{invalid_libc.c => invalid_libc.i} | 0
.../tests/erroneous/{no-libc.c => no-libc.i} | 0
.../tests/erroneous/{no-param.c => no-param.i} | 0
.../erroneous/{not-enough-par.c => not-enough-par.i} | 0
.../tests/erroneous/oracle/invalid_libc.res.oracle | 6 +++---
.../tests/erroneous/oracle/no-libc.res.oracle | 4 ++--
.../tests/erroneous/oracle/not-enough-par.res.oracle | 5 ++---
.../erroneous/oracle/variadic-builtin.res.oracle | 2 +-
.../{variadic-builtin.c => variadic-builtin.i} | 0
.../tests/known/oracle/printf_redefined.res.oracle | 6 +++---
.../known/{printf_redefined.c => printf_redefined.i} | 0
41 files changed, 57 insertions(+), 58 deletions(-)
rename src/plugins/variadic/tests/declared/{empty-vpar-with-ghost.c => empty-vpar-with-ghost.i} (100%)
rename src/plugins/variadic/tests/declared/{empty-vpar.c => empty-vpar.i} (100%)
rename src/plugins/variadic/tests/declared/{function-ptr-with-ghost.c => function-ptr-with-ghost.i} (100%)
rename src/plugins/variadic/tests/declared/{label.c => label.i} (100%)
rename src/plugins/variadic/tests/declared/{multi.c => multi.i} (100%)
rename src/plugins/variadic/tests/declared/{no-va-with-ghost.c => no-va-with-ghost.i} (100%)
rename src/plugins/variadic/tests/declared/{no-va.c => no-va.i} (100%)
rename src/plugins/variadic/tests/declared/{rvalues-with-ghost.c => rvalues-with-ghost.i} (100%)
rename src/plugins/variadic/tests/declared/{rvalues.c => rvalues.i} (100%)
rename src/plugins/variadic/tests/declared/{simple-with-ghost.c => simple-with-ghost.i} (100%)
rename src/plugins/variadic/tests/declared/{simple.c => simple.i} (100%)
rename src/plugins/variadic/tests/declared/{struct.c => struct.i} (100%)
rename src/plugins/variadic/tests/declared/{typedefed_function-with-ghost.c => typedefed_function-with-ghost.i} (100%)
rename src/plugins/variadic/tests/declared/{typedefed_function.c => typedefed_function.i} (100%)
rename src/plugins/variadic/tests/defined/{recursive.c => recursive.i} (100%)
rename src/plugins/variadic/tests/erroneous/{invalid_libc.c => invalid_libc.i} (100%)
rename src/plugins/variadic/tests/erroneous/{no-libc.c => no-libc.i} (100%)
rename src/plugins/variadic/tests/erroneous/{no-param.c => no-param.i} (100%)
rename src/plugins/variadic/tests/erroneous/{not-enough-par.c => not-enough-par.i} (100%)
rename src/plugins/variadic/tests/erroneous/{variadic-builtin.c => variadic-builtin.i} (100%)
rename src/plugins/variadic/tests/known/{printf_redefined.c => printf_redefined.i} (100%)
diff --git a/src/plugins/variadic/tests/declared/empty-vpar-with-ghost.c b/src/plugins/variadic/tests/declared/empty-vpar-with-ghost.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/empty-vpar-with-ghost.c
rename to src/plugins/variadic/tests/declared/empty-vpar-with-ghost.i
diff --git a/src/plugins/variadic/tests/declared/empty-vpar.c b/src/plugins/variadic/tests/declared/empty-vpar.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/empty-vpar.c
rename to src/plugins/variadic/tests/declared/empty-vpar.i
diff --git a/src/plugins/variadic/tests/declared/function-ptr-with-ghost.c b/src/plugins/variadic/tests/declared/function-ptr-with-ghost.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/function-ptr-with-ghost.c
rename to src/plugins/variadic/tests/declared/function-ptr-with-ghost.i
diff --git a/src/plugins/variadic/tests/declared/label.c b/src/plugins/variadic/tests/declared/label.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/label.c
rename to src/plugins/variadic/tests/declared/label.i
diff --git a/src/plugins/variadic/tests/declared/multi.c b/src/plugins/variadic/tests/declared/multi.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/multi.c
rename to src/plugins/variadic/tests/declared/multi.i
diff --git a/src/plugins/variadic/tests/declared/no-va-with-ghost.c b/src/plugins/variadic/tests/declared/no-va-with-ghost.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/no-va-with-ghost.c
rename to src/plugins/variadic/tests/declared/no-va-with-ghost.i
diff --git a/src/plugins/variadic/tests/declared/no-va.c b/src/plugins/variadic/tests/declared/no-va.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/no-va.c
rename to src/plugins/variadic/tests/declared/no-va.i
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 5735fe81560..66bd6f7bb1c 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,11 @@
-[variadic] tests/declared/empty-vpar-with-ghost.c:1:
+[variadic] tests/declared/empty-vpar-with-ghost.i:1:
Declaration of variadic function f.
-[variadic] tests/declared/empty-vpar-with-ghost.c:8:
+[variadic] tests/declared/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.c:8: Warning:
+[kernel] tests/declared/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 0603bbc1ab9..c028e9e151d 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,10 @@
-[variadic] tests/declared/empty-vpar.c:1: Declaration of variadic function f.
-[variadic] tests/declared/empty-vpar.c:8:
+[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.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[kernel] tests/declared/empty-vpar.c:8: Warning:
+[kernel] tests/declared/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 d23f5b52381..b3aa3b62aef 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,11 @@
-[variadic] tests/declared/function-ptr-with-ghost.c:4:
+[variadic] tests/declared/function-ptr-with-ghost.i:4:
Declaration of variadic function va_f.
-[variadic] tests/declared/function-ptr-with-ghost.c:2:
+[variadic] tests/declared/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.c:2: Warning:
+[kernel:annot:missing-spec] tests/declared/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 0c517829175..427868a9c76 100644
--- a/src/plugins/variadic/tests/declared/oracle/label.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/label.res.oracle
@@ -1,10 +1,10 @@
-[variadic] tests/declared/label.c:4: Declaration of variadic function f.
-[variadic] tests/declared/label.c:8:
+[variadic] tests/declared/label.i:4: Declaration of variadic function f.
+[variadic] tests/declared/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.c:8: Warning:
+[kernel:annot:missing-spec] tests/declared/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 58b1c09b383..adcbb2b04d4 100644
--- a/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
@@ -1,16 +1,16 @@
-[variadic] tests/declared/multi.c:1: Declaration of variadic function f.
-[variadic] tests/declared/multi.c:12: Declaration of variadic function g.
-[variadic] tests/declared/multi.c:9:
+[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.c:18:
+[variadic] tests/declared/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.c:18: Warning:
+[kernel] tests/declared/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.c:9: Warning:
+[kernel] tests/declared/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 ddd747806b9..472fa003177 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.c:4: Warning:
+[kernel:annot:missing-spec] tests/declared/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 df93a80eca4..f00b72688a6 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.c:4: Warning:
+[kernel:annot:missing-spec] tests/declared/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 ba5af06214b..ce15956f751 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,11 @@
-[variadic] tests/declared/rvalues-with-ghost.c:1:
+[variadic] tests/declared/rvalues-with-ghost.i:1:
Declaration of variadic function f.
-[variadic] tests/declared/rvalues-with-ghost.c:5:
+[variadic] tests/declared/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.c:5: Warning:
+[kernel:annot:missing-spec] tests/declared/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 99e27480afa..82863e34c74 100644
--- a/src/plugins/variadic/tests/declared/oracle/rvalues.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/rvalues.res.oracle
@@ -1,10 +1,10 @@
-[variadic] tests/declared/rvalues.c:1: Declaration of variadic function f.
-[variadic] tests/declared/rvalues.c:5:
+[variadic] tests/declared/rvalues.i:1: Declaration of variadic function f.
+[variadic] tests/declared/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.c:5: Warning:
+[kernel:annot:missing-spec] tests/declared/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 d4ffc72273c..3a596a240dd 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,11 @@
-[variadic] tests/declared/simple-with-ghost.c:1:
+[variadic] tests/declared/simple-with-ghost.i:1:
Declaration of variadic function f.
-[variadic] tests/declared/simple-with-ghost.c:9:
+[variadic] tests/declared/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.c:9: Warning:
+[kernel] tests/declared/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 d36878734cf..9112e947007 100644
--- a/src/plugins/variadic/tests/declared/oracle/simple.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/simple.res.oracle
@@ -1,10 +1,10 @@
-[variadic] tests/declared/simple.c:1: Declaration of variadic function f.
-[variadic] tests/declared/simple.c: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.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[kernel] tests/declared/simple.c:9: Warning:
+[kernel] tests/declared/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 37d0817d12f..851c21816f4 100644
--- a/src/plugins/variadic/tests/declared/oracle/struct.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/struct.res.oracle
@@ -1,10 +1,10 @@
-[variadic] tests/declared/struct.c:5: Declaration of variadic function f.
-[variadic] tests/declared/struct.c:10:
+[variadic] tests/declared/struct.i:5: Declaration of variadic function f.
+[variadic] tests/declared/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.c:10: Warning:
+[kernel:annot:missing-spec] tests/declared/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 2608a327a0b..2b4685e9792 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.c:2:
+[variadic] tests/declared/typedefed_function-with-ghost.i:2:
Declaration of variadic function f.
-[variadic] tests/declared/typedefed_function-with-ghost.c:5:
+[variadic] tests/declared/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.c:5: Warning:
+[kernel:annot:missing-spec] tests/declared/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 b497ee3c477..fa5cdfe98bb 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,11 @@
-[variadic] tests/declared/typedefed_function.c:2:
+[variadic] tests/declared/typedefed_function.i:2:
Declaration of variadic function f.
-[variadic] tests/declared/typedefed_function.c:5:
+[variadic] tests/declared/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.c:5: Warning:
+[kernel:annot:missing-spec] tests/declared/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/declared/rvalues-with-ghost.c b/src/plugins/variadic/tests/declared/rvalues-with-ghost.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/rvalues-with-ghost.c
rename to src/plugins/variadic/tests/declared/rvalues-with-ghost.i
diff --git a/src/plugins/variadic/tests/declared/rvalues.c b/src/plugins/variadic/tests/declared/rvalues.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/rvalues.c
rename to src/plugins/variadic/tests/declared/rvalues.i
diff --git a/src/plugins/variadic/tests/declared/simple-with-ghost.c b/src/plugins/variadic/tests/declared/simple-with-ghost.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/simple-with-ghost.c
rename to src/plugins/variadic/tests/declared/simple-with-ghost.i
diff --git a/src/plugins/variadic/tests/declared/simple.c b/src/plugins/variadic/tests/declared/simple.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/simple.c
rename to src/plugins/variadic/tests/declared/simple.i
diff --git a/src/plugins/variadic/tests/declared/struct.c b/src/plugins/variadic/tests/declared/struct.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/struct.c
rename to src/plugins/variadic/tests/declared/struct.i
diff --git a/src/plugins/variadic/tests/declared/typedefed_function-with-ghost.c b/src/plugins/variadic/tests/declared/typedefed_function-with-ghost.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/typedefed_function-with-ghost.c
rename to src/plugins/variadic/tests/declared/typedefed_function-with-ghost.i
diff --git a/src/plugins/variadic/tests/declared/typedefed_function.c b/src/plugins/variadic/tests/declared/typedefed_function.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/typedefed_function.c
rename to src/plugins/variadic/tests/declared/typedefed_function.i
diff --git a/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle b/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle
index 90e4c436eef..9fcbfae2ed2 100644
--- a/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle
@@ -1,14 +1,14 @@
-[variadic] tests/defined/recursive.c:4: Declaration of variadic function f.
-[variadic] tests/defined/recursive.c:8:
+[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.c:12:
+[variadic] tests/defined/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.c:8: Warning:
+[eva] tests/defined/recursive.i:8: Warning:
recursive call during value analysis
- of f (f <- f :: tests/defined/recursive.c:12 <- main). Assuming the call has
+ of f (f <- f :: tests/defined/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
diff --git a/src/plugins/variadic/tests/defined/recursive.c b/src/plugins/variadic/tests/defined/recursive.i
similarity index 100%
rename from src/plugins/variadic/tests/defined/recursive.c
rename to src/plugins/variadic/tests/defined/recursive.i
diff --git a/src/plugins/variadic/tests/erroneous/invalid_libc.c b/src/plugins/variadic/tests/erroneous/invalid_libc.i
similarity index 100%
rename from src/plugins/variadic/tests/erroneous/invalid_libc.c
rename to src/plugins/variadic/tests/erroneous/invalid_libc.i
diff --git a/src/plugins/variadic/tests/erroneous/no-libc.c b/src/plugins/variadic/tests/erroneous/no-libc.i
similarity index 100%
rename from src/plugins/variadic/tests/erroneous/no-libc.c
rename to src/plugins/variadic/tests/erroneous/no-libc.i
diff --git a/src/plugins/variadic/tests/erroneous/no-param.c b/src/plugins/variadic/tests/erroneous/no-param.i
similarity index 100%
rename from src/plugins/variadic/tests/erroneous/no-param.c
rename to src/plugins/variadic/tests/erroneous/no-param.i
diff --git a/src/plugins/variadic/tests/erroneous/not-enough-par.c b/src/plugins/variadic/tests/erroneous/not-enough-par.i
similarity index 100%
rename from src/plugins/variadic/tests/erroneous/not-enough-par.c
rename to src/plugins/variadic/tests/erroneous/not-enough-par.i
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 de3bfcfe76b..321767e5220 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,7 @@
-[variadic] tests/erroneous/invalid_libc.c:2:
+[variadic] tests/erroneous/invalid_libc.i:2:
Declaration of variadic function fprintf.
-[variadic] tests/erroneous/invalid_libc.c:2: Warning:
+[variadic] tests/erroneous/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.c:6:
+[variadic] tests/erroneous/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 121d95f029c..64101cd01a7 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.c:1: Declaration of variadic function printf.
+[variadic] tests/erroneous/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.c:5:
+[variadic] tests/erroneous/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 82b74398907..c05a4ba9b29 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,5 +1,4 @@
-[kernel] tests/erroneous/not-enough-par.c:4: User Error:
+[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.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
+[kernel] User Error: stopping on file "tests/erroneous/not-enough-par.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
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 780e418ed94..30f7e2cf18c 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.c:1:
+[variadic] tests/erroneous/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 http://bts.frama-c.com with:
diff --git a/src/plugins/variadic/tests/erroneous/variadic-builtin.c b/src/plugins/variadic/tests/erroneous/variadic-builtin.i
similarity index 100%
rename from src/plugins/variadic/tests/erroneous/variadic-builtin.c
rename to src/plugins/variadic/tests/erroneous/variadic-builtin.i
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 9b7494fd834..41b4f0c4fb8 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,10 @@
-[variadic] tests/known/printf_redefined.c:3:
+[variadic] tests/known/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.c:7:
+[variadic] tests/known/printf_redefined.i:7:
Translating call to printf to a call to the specialized version printf_va_1.
-[variadic] tests/known/printf_redefined.c:7: Warning:
+[variadic] tests/known/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/printf_redefined.c b/src/plugins/variadic/tests/known/printf_redefined.i
similarity index 100%
rename from src/plugins/variadic/tests/known/printf_redefined.c
rename to src/plugins/variadic/tests/known/printf_redefined.i
--
GitLab