From 4d5d4f62a72cad043c4ca3da8d2b93d59cd1eb44 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 3 Feb 2022 23:49:29 +0100
Subject: [PATCH] [analysis-scripts] add test for estimate-difficulty
---
tests/fc_script/estimate_difficulty.i | 28 +++++++++++++++++++
.../fc_script/oracle/estimate_difficulty.err | 0
.../fc_script/oracle/estimate_difficulty.res | 11 ++++++++
tests/fc_script/oracle/find_fun1.res | 2 +-
tests/fc_script/oracle/find_fun2.res | 2 +-
tests/fc_script/oracle/find_fun3.res | 2 +-
6 files changed, 42 insertions(+), 3 deletions(-)
create mode 100644 tests/fc_script/estimate_difficulty.i
create mode 100644 tests/fc_script/oracle/estimate_difficulty.err
create mode 100644 tests/fc_script/oracle/estimate_difficulty.res
diff --git a/tests/fc_script/estimate_difficulty.i b/tests/fc_script/estimate_difficulty.i
new file mode 100644
index 00000000000..23b63dd6c52
--- /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 00000000000..e69de29bb2d
diff --git a/tests/fc_script/oracle/estimate_difficulty.res b/tests/fc_script/oracle/estimate_difficulty.res
new file mode 100644
index 00000000000..6b197b72414
--- /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 f16fc61d2be..58bf804e3c1 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 fda8345bfc2..d868795ee4e 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 4a42d911708..00f4bbc10ea 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'
--
GitLab