diff --git a/src/plugins/variadic/.gitignore b/src/plugins/variadic/.gitignore index 0114e3d0f08985bcf97727dcde8f314ddb4410ae..b18adc61b4fbcc6e775225047b0a86a8a8a8659d 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 7d6ccc4f7f67ae5be501a3d5806fb645b6219623..31352e2ab42d27b76e2610a2e8a239023e21a667 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 9d66c6a41ea99002a90858d315f8e28c160fcd49..9957113d4d7eb8bc898109f1c3fa6ede8525da31 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 77d342b3dd8113ce3c181cca5993138243e6bbe4..1a0792c2ff9443783157516d91a6e3c194b263eb 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 c028e9e151d91ac8f3d848668a9ead0863bef9f1..34cb206144215e6ceb008595bc0e513e4562463b 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 f81ac2a39cfd228c91a75b2f1f0ea81f0c32a683..c6a56c0319e4234140e82b03a915ee68f7c25c6d 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 427868a9c76ae47b935ff087454c0ef2b589dc3d..e4256555494a18c88a9c3e97456303f956aabaeb 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 adcbb2b04d43ce39487600c92e43c8f4c6d65a55..cb244196e322669339ed9da049566249afc0db47 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 71fffe6ce3458de80a11bed3ab9404ef530b1137..abfb5632e9a448a87be8e4b5237579db5aea3270 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 f00b72688a6be12492c6b91ac8db6c8ab0a43dcc..df9bae19b0939012d7a9ecd38c63703a42c4fbd7 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 9dde9d6d2dfbaa061b976f6f32aa14042c6fa493..deaa01bb980f5d548526b0ea84d6f724dba6c4a9 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 82863e34c748ad7430e51e9490d9e1cdefa51f28..9570cd50b5da9f747d57ff2e65f1349b97a7cf5f 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 fa2e63b8a114173eac0d131f2fe7c203d8ef6592..f67021d13bfad44ba0060770645569b29440957a 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 9112e9470077a769eaa504faed32bb9cf3caf757..d605019696f536e657f92845f96a4961b78681af 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 851c21816f4c535bc3c0e443d014611b540c9768..2f716c490cd3198d6418af7618162fe0be7f04d9 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 3038502c8ded9a4b0149591a360b55e8c7118292..94bbdbea2a1c25b2de228ca6137fdb9acd25c913 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 fa5cdfe98bbd3fb99d79eaceab46e2b687038d64..f3795220e5db86b2d1bba7573750aba40356a30e 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 208a9cae21b756cd30ca8b051b1eb1b8807c38f6..5e9804ebfaec6636933069705d5d095067a4ebe6 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 1a7b9cd9cf2d9bf1023003d192f3f6a794512d4f..7a925bc77a1709a00900656e67040c18ceb6275a 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 7f338532acdc46cb6ab68dfd84819601cf787197..c908a44a0498e785bec9061aae4e121ff9026da2 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 a7b3971db2a4c52c818065884c15d0e53fcb0e66..1ad1f6de266ce5e9da9d1a71b371189f200ad0ac 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 ded04c65a71a2325e204765ab517b6285fd3fda3..fdbc4879d71839464935389de8c95f3e63ec1ce3 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 7369a68d0b2dff785f411483c5f39da4584de845..ed8db7e16c2c76851c57c5f18703ec0388a7438c 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 0bc3f144390573516f1965b8d5b4e9df34944ff4..fcfbf225ed1fce344f840f7005069ab41e1ff1e5 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 9fcbfae2ed2afb6f4498cd8fc01efebb747ea53f..2fb73b23782cfccbfc3e6583baba92c843ac1d16 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 a2ee2ed266c1387055e819f4b2e4e3140c260261..5d7fc79ffbb2f8ca1162dd084b0b3e27fd9e4f4d 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 44c52cd1b73640e3ea054e44b82a79f6b48f2b12..66ca05b979890b76bcd32c42a58475e1d5c7a2d1 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 e65d36e637b8b349c7431136d307c68622bfdad9..63a0918d464ceb7c20dba8f66cc0ce2cf97f762d 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 83a0ba4f9cf11e5afd51b149f043b7ed155f2658..9555e18f785dde9f7d2049cfb8c922e47ca3c056 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 5fc590007e57e1a9c02fabfa279c7f055923488f..e60bb9ef10ae3763f5aa68c5c6316fdba0b70a14 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 a1cffb94e46af0146e39f33ff418129358bf9178..d61d275a2e53fcc956afef08f597bd3128613e57 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 321767e52205d5455405b950258b4c4928dab8cd..c830fa3b1f625ba9217e8984e852683ba2e6bc94 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 64101cd01a75097315b353cb57906d47cfb2b087..6f2256ced8458c2138a064fe059fd90219d985e2 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 c05a4ba9b29af3af3f01dcbf46d240984404e5b4..74cb88e414fb8c65a0d7a479d861b8ce10c82aff 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 bf32832912efc4f3b07515090655826e888ce94c..b1fafb7e3bc44f66f23cfa740120f7a554bed3ba 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 63b857583a242aae76f100f8347641b631c5a229..ff77e4725d8caba6826723de769b2d76696e7180 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 7af1312eace35e3f68a49d3479fb7a3dcdcb9083..9688df149a0e661870cf030779bbfadaaa883318 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 d42e13c1ae8463c3923c3ff795491571140e2a2f..e5210fc9b6befc3db729f23cfcdc90e9b0f7d9c2 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 956067e6dbe9bc926d55bc7e9ce53dea74f565d3..496a4c83bbcde25cdcbade988260628a40c6e6f3 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 47d6f5693dc5bbb245732803a89a277b5287f17b..e7fb761c8dcb9868143cd6b5aa64836f0f25e499 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 529a1b844f24e9b2005e75a13d74ee945f0a6d85..b2369bbf643aee5bf7d2d7dedb56930657f30128 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 195847c4a798c48e04d7613f0a9ff77e106c4001..f7eb492e339bf8ebf8a0dc9a5b45c88dc3168ee4 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 840ef4ab762032796a9e8a0e13459ae0745de421..0fcb6724a858b2c6a145ac364f7b1de54ff98f7f 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 b7200eb4eb8fbcffa86d9be93399bc29551da793..eeb1928dbf300bab138a41a983c6013b3e25d8fb 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 045316f712aebc6d8f0ff79b5b7f84d9140ccff0..daaa34b4a43db6294e6e7c5409d5c36fa3a4c325 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 fcce6d0115732a749b8a8923723a7243c9dfb804..ed919acd377b4bdd0ee1f685fa684ab1b648d60d 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 d7102dda0aa118a8915a12b3801847c657c4016e..8d14fdb2e91b9e1fa0102fc8c45c02678b7aecbc 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 e75911730236bc2264e15e690bbe63de68d9e92b..e0bb8251627730b6cd338b9ddb912acc614b1f89 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 41b4f0c4fb811f31682c40d4a3d82aba5efd6ef7..a646cae3da3383e57d8dc67dab11b006c9106afd 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 4ee27be46611b179b94c9eca126c0a3aed8a46e3..804a65eac3d205d950421b36de450711e22228a5 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 2c72bbbab0497dc928525540fbe32d744e90c774..e7020976a8b1a8b0115c94246acc40b7f7d24856 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 5d41306e7d7770b2f2debc89711360675aa0bdc1..e523ee334bcb0a5ea0cd19f000fc4b4c8145d9c0 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 bf4a9d81548e13066cc07874387d684d28e89997..af4cc6e94af5b4e5cb5b7b471c6ccc556764863e 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 e563ba2f274de6ca32bf4384ba1c876d0d3fed51..fa1b0a80a48930f01a07db201c9e20d26e712298 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 704b3de7532cbbe3b74de18a9b261d8fb1990a4b..7ecea7ad0fcd57ee3cc17be198d733f3c7a508cd 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 cecc5cc54317c70556a4191b957dfffa35b3ab2b..e51a5c3ce8ad3e2678658be7a9624cd41bd5c5f3 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 cc3c40be6d63726412cc1680892eec9481895efa..2465387928b0f6e43c6f5ae77e7a9c9116075bee 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 f157c9d36bf492d0950438e324ebd2081d5bfa52..21d76e6c0eaf5d5ac79ccdb9a4c95a75aa8130ed 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 585983473b2a34fb414ff248ba31750429cd90cf..5fa13ac427e09a8301be5db6b1c45e26210a2007 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 b85bb1c1d0672bd3a723c7e2b659c56ed8f769c0..11cacf32ca26ea478bb7edc29b672607ecff1657 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 265018f2c74c6d406a2f0b2e28e6866fe3dc03af..db33468ad75ed8427ad04ea5c0c30a2746061193 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 0000000000000000000000000000000000000000..6fa0daf0fa10fa7fcda7f5e2257ca0071a489cd1 --- /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 e076935b23463006f8f89ffcddb93f7f2748c691..3a9dd329444670bb5233806a1741d750826da077 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