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 5735fe8156033fe195ffbaed2f2bf33871e65f61..66bd6f7bb1cb706d4de76f900970c95e7e8ccee9 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 0603bbc1ab9646011fbd050407523a1a8fddf452..c028e9e151d91ac8f3d848668a9ead0863bef9f1 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 d23f5b523810e4f0743338a780bb6d9041a04d43..b3aa3b62aef8c3f6d560fe83d3e81496cdfac3fb 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 0c51782917566ef261529445f19a27d6fa5749b2..427868a9c76ae47b935ff087454c0ef2b589dc3d 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 58b1c09b3834a3614654b7116de3ec709e16417d..adcbb2b04d43ce39487600c92e43c8f4c6d65a55 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 ddd747806b958ade5a116ccacfe93652561a2bfa..472fa003177f2145a70fb5341fd12b96b6067a4b 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 df93a80eca42e87351c30aa535b2914f7cd8cd48..f00b72688a6be12492c6b91ac8db6c8ab0a43dcc 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 ba5af06214b5fa1c26636c4dec73ede26ff36d16..ce15956f7514b963da8de6ba63e5fc6c1d56a700 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 99e27480afacce5296c6d5d0e4b2c5c5f387200f..82863e34c748ad7430e51e9490d9e1cdefa51f28 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 d4ffc72273c5b8619dcf31832435920b2372181c..3a596a240ddb042bac22384b3267f26a13fcbbae 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 d36878734cf263a85f28807227f051986d50fac3..9112e9470077a769eaa504faed32bb9cf3caf757 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 37d0817d12f1fd03bf5342a582c78716c10e7749..851c21816f4c535bc3c0e443d014611b540c9768 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 2608a327a0b7f30ba64bd0f20d37281bf652593f..2b4685e9792f6357f8f3d061bb4b5964d99b1f22 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 b497ee3c477f455d1f22aad98c26929e4a251716..fa5cdfe98bbd3fb99d79eaceab46e2b687038d64 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 90e4c436eef05876c5fa6f7a399d1ed24a7a8cc9..9fcbfae2ed2afb6f4498cd8fc01efebb747ea53f 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 de3bfcfe76b1ff09db17d7ec9e9bc67d88a32627..321767e52205d5455405b950258b4c4928dab8cd 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 121d95f029cf9c1cb126173e22f4dee7ec656c8a..64101cd01a75097315b353cb57906d47cfb2b087 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 82b7439890793d48dc358156d48bcee6e153366e..c05a4ba9b29af3af3f01dcbf46d240984404e5b4 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 780e418ed94a3b3f92cfd3721e4789ae5b6c793f..30f7e2cf18c5d3543616fe729f4c0856b7693785 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 9b7494fd8342d16b8e56adb562b395d9c87edb25..41b4f0c4fb811f31682c40d4a3d82aba5efd6ef7 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