diff --git a/tests/fc_script/estimate_difficulty.i b/tests/fc_script/estimate_difficulty.i new file mode 100644 index 0000000000000000000000000000000000000000..23b63dd6c5250076eb5eb8e74f0197b0bd9a12cc --- /dev/null +++ b/tests/fc_script/estimate_difficulty.i @@ -0,0 +1,28 @@ +/* run.config + NOFRAMAC: testing frama-c-script, not frama-c itself + EXECNOW: LOG @PTEST_NAME@.res LOG @PTEST_NAME@.err PTESTS_TESTING=1 %{bin:frama-c-script} estimate-difficulty @PTEST_FILE@ > @PTEST_NAME@.res 2> @PTEST_NAME@.err +*/ + +// these includes are not actually used by the compiler +// (this is a preprocessed file), but analyzed by the script +#include <sys/socket.h> +# include <complex.h> + # include <langinfo.h> +#include <sys/socket.h> + +void g() { + int g = 42; +} + +void f() { + if (v) f(); + else g(); +} + +int main() { + va_arg(); // no warning: it is a macro, not a function + setjmp(); // warning: problematic + strlen(); // no warning + ccosl(); // warning: neither code nor spec + dprintf(); // no warning: neither code nor spec, but handled by Variadic +} diff --git a/tests/fc_script/oracle/estimate_difficulty.err b/tests/fc_script/oracle/estimate_difficulty.err new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/tests/fc_script/oracle/estimate_difficulty.res b/tests/fc_script/oracle/estimate_difficulty.res new file mode 100644 index 0000000000000000000000000000000000000000..6b197b724146d7ba3507c29a2979df06f1027627 --- /dev/null +++ b/tests/fc_script/oracle/estimate_difficulty.res @@ -0,0 +1,11 @@ +Building callgraph... +Computing data about libc/POSIX functions... +[recursion] found recursive cycle near estimate_difficulty.i:18: f -> f +Estimating difficulty for 7 function calls... +- warning: ccosl (POSIX) has neither code nor spec in Frama-C's libc +- warning: setjmp (POSIX) is known to be problematic for code analysis +Function-related warnings: 2 +Estimating difficulty for 3 '#include <header>' directives... +- WARNING: included header <complex.h> is explicitly unsupported by Frama-C +- warning: included header <langinfo.h> not currently included in Frama-C's libc +Header-related warnings: 2 diff --git a/tests/fc_script/oracle/find_fun1.res b/tests/fc_script/oracle/find_fun1.res index f16fc61d2be3d40fae3e6b45961875fc0e7f0642..58bf804e3c123e33f21c6761b63dcefa26e2e129 100644 --- a/tests/fc_script/oracle/find_fun1.res +++ b/tests/fc_script/oracle/find_fun1.res @@ -1,4 +1,4 @@ -Looking for 'main2' inside 14 file(s)... +Looking for 'main2' inside 15 file(s)... Possible declarations for function 'main2' in the following file(s): for-find-fun.c Possible definitions for function 'main2' in the following file(s): diff --git a/tests/fc_script/oracle/find_fun2.res b/tests/fc_script/oracle/find_fun2.res index fda8345bfc224212d8b8d653d325ed83b7acac7c..d868795ee4e11b8858e75185cfd91d68ea8a24e7 100644 --- a/tests/fc_script/oracle/find_fun2.res +++ b/tests/fc_script/oracle/find_fun2.res @@ -1,4 +1,4 @@ -Looking for 'main3' inside 14 file(s)... +Looking for 'main3' inside 15 file(s)... Possible declarations for function 'main3' in the following file(s): for-find-fun2.c Possible definitions for function 'main3' in the following file(s): diff --git a/tests/fc_script/oracle/find_fun3.res b/tests/fc_script/oracle/find_fun3.res index 4a42d9117089960eb086c47a8e4b07b44795e3c3..00f4bbc10eab9c20620426e670d9d0cf6b715762 100644 --- a/tests/fc_script/oracle/find_fun3.res +++ b/tests/fc_script/oracle/find_fun3.res @@ -1,2 +1,2 @@ -Looking for 'false_positive' inside 14 file(s)... +Looking for 'false_positive' inside 15 file(s)... No declaration/definition found for function 'false_positive'