diff --git a/nix/kernel-tests.nix b/nix/kernel-tests.nix
index 3ca82c80b2459cccb879668862953a4fc013ebbb..5fa1c0096d2945ddd0d07d183dd63271c7d9f448 100644
--- a/nix/kernel-tests.nix
+++ b/nix/kernel-tests.nix
@@ -16,5 +16,7 @@ mk_tests {
@tests/syntax/ptests \
@tests/test/ptests \
@src/kernel_internals/parsing/tests/ptests
+ dune runtest \
+ tests/fc_script
'';
}
diff --git a/share/analysis-scripts/list_files.py b/share/analysis-scripts/list_files.py
index 37e5a8bc7ffba6a2ebac8897df3aed5efa6dd32b..20727d9d98f51f5361c06c4f0bf5b38a3cc2754b 100755
--- a/share/analysis-scripts/list_files.py
+++ b/share/analysis-scripts/list_files.py
@@ -80,13 +80,17 @@ print("")
files_defining_main = set()
re_main = re.compile(r"(int|void)\s+main\s*\([^)]*\)\s*\{")
-for fname, file_for_fcmake in files:
- assert os.path.exists(fname), "file does not exist: %s" % fname
- with open(fname, "r") as content_file:
- content = content_file.read()
- res = re.search(re_main, content)
- if res is not None:
- files_defining_main.add(file_for_fcmake)
+for fname, file_for_fcmake in sorted(files):
+ try:
+ with open(fname, "r") as content_file:
+ content = content_file.read()
+ res = re.search(re_main, content)
+ if res is not None:
+ files_defining_main.add(file_for_fcmake)
+ except OSError:
+ print(
+ f"warning: could not read file '{fname}', mentioned in '{arg}'. Skipping check of 'main' function."
+ )
if files_defining_main != []:
print("")
diff --git a/tests/fc_script/build-callgraph.i b/tests/fc_script/build-callgraph.t/build-callgraph.c
similarity index 78%
rename from tests/fc_script/build-callgraph.i
rename to tests/fc_script/build-callgraph.t/build-callgraph.c
index 43682ba812fb812bfad29941c729a9fc607dccec..1e235e1d4355bed11efafbe785fed75ae6fff39f 100644
--- a/tests/fc_script/build-callgraph.i
+++ b/tests/fc_script/build-callgraph.t/build-callgraph.c
@@ -1,8 +1,3 @@
-/* run.config
- NOFRAMAC: testing frama-c-script, not frama-c itself
- EXECNOW: LOG build-callgraph.res LOG build-callgraph.err PTESTS_TESTING=1 %{bin:frama-c-script} heuristic-print-callgraph %{dep:./@PTEST_NAME@.i} > ./build-callgraph.res 2> ./build-callgraph.err
- */
-
#include <stdio.h>
void main() {
strlen("");
diff --git a/tests/fc_script/build-callgraph.t/run.t b/tests/fc_script/build-callgraph.t/run.t
new file mode 100644
index 0000000000000000000000000000000000000000..dd02545e12eade57fe2b59e86a52a7351dd6685a
--- /dev/null
+++ b/tests/fc_script/build-callgraph.t/run.t
@@ -0,0 +1,22 @@
+ $ PTESTS_TESTING=1 frama-c-script heuristic-print-callgraph build-callgraph.c
+ build-callgraph.c:3: main -> strlen
+ build-callgraph.c:15: fn1 -> Frama_C_show_each_1
+ build-callgraph.c:16: fn1 -> Frama_C_show_each_2
+ build-callgraph.c:22: main1 -> fn1
+ build-callgraph.c:23: main1 -> fn2
+ build-callgraph.c:24: main1 -> Frama_C_show_each_d
+ build-callgraph.c:42: main3 -> not_a_function_call
+ build-callgraph.c:43: main3 -> yet_another_not_a_call
+ build-callgraph.c:48: main4 -> f
+ build-callgraph.c:56: main4 -> f
+ build-callgraph.c:48: main4 -> g
+ build-callgraph.c:57: main4 -> g
+ build-callgraph.c:48: main4 -> h
+ build-callgraph.c:48: main4 -> k
+ build-callgraph.c:48: main4 -> m
+ build-callgraph.c:48: main4 -> n
+ build-callgraph.c:49: main4 -> p
+ build-callgraph.c:60: main -> main1
+ build-callgraph.c:61: main -> main2
+ build-callgraph.c:62: main -> main3
+ build-callgraph.c:63: main -> main4
diff --git a/tests/fc_script/dune b/tests/fc_script/dune
new file mode 100644
index 0000000000000000000000000000000000000000..d6ebc9674e12dfb60d0a78e3212be839c3f0a536
--- /dev/null
+++ b/tests/fc_script/dune
@@ -0,0 +1,9 @@
+; Almost all frama-c-script commands require Python
+(cram
+ (enabled_if %{read:../../python-3.7-available})
+)
+
+(cram
+ (applies_to make-machdep)
+ (enabled_if (and %{bin-available:clang} %{bin-available:yq}))
+)
diff --git a/tests/fc_script/estimate_difficulty.i b/tests/fc_script/estimate-difficulty.t/estimate-difficulty.c
similarity index 61%
rename from tests/fc_script/estimate_difficulty.i
rename to tests/fc_script/estimate-difficulty.t/estimate-difficulty.c
index 68ee456b3a5a8850ca1b6dd8073e1c09a9a0cada..8a595e24c9b96bae70c579aa8b06ee518cc6b72e 100644
--- a/tests/fc_script/estimate_difficulty.i
+++ b/tests/fc_script/estimate-difficulty.t/estimate-difficulty.c
@@ -1,9 +1,3 @@
-/* run.config
- NOFRAMAC: testing frama-c-script, not frama-c itself
- COMMENT: Disabled for now, when tests are executed in parallel, this test often fails
- DONTRUN: 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>
diff --git a/tests/fc_script/estimate-difficulty.t/run.t b/tests/fc_script/estimate-difficulty.t/run.t
new file mode 100644
index 0000000000000000000000000000000000000000..01545694bb1b4fd051595a1e488270d16952036e
--- /dev/null
+++ b/tests/fc_script/estimate-difficulty.t/run.t
@@ -0,0 +1,11 @@
+ $ PTESTS_TESTING=1 frama-c-script estimate-difficulty estimate-difficulty.c
+ Building callgraph...
+ Computing data about libc/POSIX functions...
+ [recursion] found recursive cycle near estimate-difficulty.c:13: 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
+ Header-related warnings: 1
diff --git a/tests/fc_script/find-fun.t/build-callgraph.c b/tests/fc_script/find-fun.t/build-callgraph.c
new file mode 100644
index 0000000000000000000000000000000000000000..1e235e1d4355bed11efafbe785fed75ae6fff39f
--- /dev/null
+++ b/tests/fc_script/find-fun.t/build-callgraph.c
@@ -0,0 +1,64 @@
+#include <stdio.h>
+void main() {
+ strlen("");
+}
+struct s {
+ int a; int b;
+} s;
+
+volatile int v;
+
+int fn2(int, int);
+
+int fn1(int x, int y)
+{
+ Frama_C_show_each_1(x);
+ Frama_C_show_each_2(y);
+ return x + y;
+}
+
+int X, Y;
+int main1 () {
+ R1 = fn1(G, G|0);
+ R2 = fn2(G, G|0);
+ Frama_C_show_each_d(G);
+ pv = (int *) &X;
+ return Y;
+}
+
+int * main2() {
+ return 0;
+}
+
+#define not_a_function_call(v) \
+ yes_a_function_call(v)
+
+#define yet_another_not_a_call(v) do { \
+ yes_again(); \
+ } while (0)
+
+/* call_inside_comment(evaluation); */
+void main3 () {
+ //@ not_a_function_call(v);
+ yet_another_not_a_call(v);
+}
+
+/* Tests the initialization of local variables. */
+void main4 () {
+ f(g(h(i, j), k (l, m ( n(
+ o, p(
+ q)
+ )
+ )
+ )
+ )
+ );
+ f();
+ g();
+}
+void main() {
+ main1();
+ main2();
+ main3();
+ main4();
+}
diff --git a/tests/fc_script/for-find-fun.c b/tests/fc_script/find-fun.t/find-fun.c
similarity index 73%
rename from tests/fc_script/for-find-fun.c
rename to tests/fc_script/find-fun.t/find-fun.c
index c8c3a67560fb5a5f321117bedacb256b8884decb..2e7404d8bb4a24feaa072e5088e4806aa5402168 100644
--- a/tests/fc_script/for-find-fun.c
+++ b/tests/fc_script/find-fun.t/find-fun.c
@@ -1,7 +1,3 @@
-/* run.config
- DONTRUN: test run by main.c
-*/
-
int
main2
(char *c, int i);
diff --git a/tests/fc_script/for-find-fun2.c b/tests/fc_script/find-fun.t/find-fun2.c
similarity index 91%
rename from tests/fc_script/for-find-fun2.c
rename to tests/fc_script/find-fun.t/find-fun2.c
index 45c8130a3683d16398c6bb839f3344fa151c9ce7..9bf89918db1f250310a2357de6e0cc7133c15e82 100644
--- a/tests/fc_script/for-find-fun2.c
+++ b/tests/fc_script/find-fun.t/find-fun2.c
@@ -1,7 +1,3 @@
-/* run.config
- DONTRUN: test run by main.c
-*/
-
struct s ** main3(
struct s *p1, struct s s2
) ;
diff --git a/tests/fc_script/for-list-functions.c b/tests/fc_script/find-fun.t/list-functions.c
similarity index 69%
rename from tests/fc_script/for-list-functions.c
rename to tests/fc_script/find-fun.t/list-functions.c
index 44ec1ad26863049872816ce4d4003b21e56693de..a71c42a5419902342063bc2823348d09edf00df9 100644
--- a/tests/fc_script/for-list-functions.c
+++ b/tests/fc_script/find-fun.t/list-functions.c
@@ -1,9 +1,5 @@
-/* run.config
- DONTRUN: test run by main.c
-*/
-
-#include "for-list-functions2.h"
-#include "for-list-functions.h"
+#include "list-functions2.h"
+#include "list-functions.h"
static int static_fun() {
static int init = 0;
diff --git a/tests/fc_script/find-fun.t/main.c b/tests/fc_script/find-fun.t/main.c
new file mode 100644
index 0000000000000000000000000000000000000000..153f05566005b05b8f14e36024a18fef0be1327b
--- /dev/null
+++ b/tests/fc_script/find-fun.t/main.c
@@ -0,0 +1,3 @@
+void main() {
+
+}
diff --git a/tests/fc_script/main2.c b/tests/fc_script/find-fun.t/main2.c
similarity index 51%
rename from tests/fc_script/main2.c
rename to tests/fc_script/find-fun.t/main2.c
index 14696dfe3472a58e4dea2770e9644c1b08a10509..1112eff2ded306e8f3248bd30f997464ed430a15 100644
--- a/tests/fc_script/main2.c
+++ b/tests/fc_script/find-fun.t/main2.c
@@ -1,8 +1,3 @@
-/* run.config
- DONTRUN:
- COMMENT: used by main.c
- */
-
void fake_main() {
}
diff --git a/tests/fc_script/find-fun.t/main3.c b/tests/fc_script/find-fun.t/main3.c
new file mode 100644
index 0000000000000000000000000000000000000000..fc9ce92c7d7c43c39dd1f7b6acaeaa2afd3f0706
--- /dev/null
+++ b/tests/fc_script/find-fun.t/main3.c
@@ -0,0 +1,4 @@
+int main( int argc, char *argv[] )
+{
+
+}
diff --git a/tests/fc_script/find-fun.t/make-wrapper.c b/tests/fc_script/find-fun.t/make-wrapper.c
new file mode 100644
index 0000000000000000000000000000000000000000..61fd6c259a1d7c85b7f0f475ba1df5b92eadf73b
--- /dev/null
+++ b/tests/fc_script/find-fun.t/make-wrapper.c
@@ -0,0 +1,21 @@
+int defined(int a);
+
+int specified(int a);
+
+int external(int a);
+
+int large_name_to_force_line_break_in_stack_msg(void) {
+ return large_name_to_force_line_break_in_stack_msg();
+}
+
+int rec(void) {
+ return large_name_to_force_line_break_in_stack_msg();
+}
+
+int main() {
+ int a = 42;
+ a = rec();
+ a = defined(a);
+ a = specified(a);
+ a = external(a);
+}
diff --git a/tests/fc_script/find-fun.t/make-wrapper2.c b/tests/fc_script/find-fun.t/make-wrapper2.c
new file mode 100644
index 0000000000000000000000000000000000000000..443b405d3cf6ab856ad9cba55b9d17aec938d44e
--- /dev/null
+++ b/tests/fc_script/find-fun.t/make-wrapper2.c
@@ -0,0 +1,12 @@
+int defined(int a) {
+ return a + 1;
+}
+
+/*@
+ assigns \result \from a;
+ ensures \result == a + 2;
+ */
+int specified(int a);
+
+// defined in another, non-included, file
+int external(int a);
diff --git a/tests/fc_script/find-fun.t/make-wrapper3.c b/tests/fc_script/find-fun.t/make-wrapper3.c
new file mode 100644
index 0000000000000000000000000000000000000000..9e04031a275ed6dd6a4268d47a79b42ef0ea021f
--- /dev/null
+++ b/tests/fc_script/find-fun.t/make-wrapper3.c
@@ -0,0 +1,5 @@
+// This file contains a definition for function 'external', but it is _not_
+// included when parsing 'make-wrapper.c'. This triggers a make-wrapper message.
+int external(int a) {
+ return a + 3;
+}
diff --git a/tests/fc_script/find-fun.t/run.t b/tests/fc_script/find-fun.t/run.t
new file mode 100644
index 0000000000000000000000000000000000000000..b7a9630d9124a819be3eaf76fca12e390c18754e
--- /dev/null
+++ b/tests/fc_script/find-fun.t/run.t
@@ -0,0 +1,19 @@
+ $ frama-c-script find-fun main2 .
+ Looking for 'main2' inside 10 file(s)...
+ Possible declarations for function 'main2' in the following file(s):
+ find-fun.c
+ Possible definitions for function 'main2' in the following file(s):
+ build-callgraph.c
+ main2.c
+
+ $ frama-c-script find-fun main3 .
+ Looking for 'main3' inside 10 file(s)...
+ Possible declarations for function 'main3' in the following file(s):
+ find-fun2.c
+ Possible definitions for function 'main3' in the following file(s):
+ build-callgraph.c
+ find-fun.c
+
+ $ frama-c-script find-fun false_positive .
+ Looking for 'false_positive' inside 10 file(s)...
+ No declaration/definition found for function 'false_positive'
diff --git a/tests/fc_script/flamegraph.txt b/tests/fc_script/flamegraph.t/flamegraph.txt
similarity index 100%
rename from tests/fc_script/flamegraph.txt
rename to tests/fc_script/flamegraph.t/flamegraph.txt
diff --git a/tests/fc_script/flamegraph.t/run.t b/tests/fc_script/flamegraph.t/run.t
new file mode 100644
index 0000000000000000000000000000000000000000..f901c56f0d2d180bdb6627b31632b8c3f2007e09
--- /dev/null
+++ b/tests/fc_script/flamegraph.t/run.t
@@ -0,0 +1,19 @@
+ $ NOGUI=1 frama-c-script flamegraph flamegraph.txt
+
+Check if the HTML file was generated
+ $ cat .frama-c/flamegraph.html
+ <!DOCTYPE html>
+ <html lang="en">
+ <head>
+ <meta charset="utf-8">
+ <title>Eva Flamegraph</title>
+ </head>
+ <body>
+ <embed src="flamegraph.svg" style="max-width:100%;width:1400px;min-width:1000px">
+ </body>
+ </html>
+
+The generated SVG is too large, so we arbitrarily grep a few lines
+ $ grep f1 .frama-c/flamegraph.svg
+ <title>f1 (6 samples, 44.44%)</title><rect x="112.2" y="65" width="664.5" height="15.0" fill="rgb(232,181,30)" rx="2" ry="2" />
+ <text text-anchor="" x="115.22" y="75.5" font-size="11" font-family="Verdana" fill="rgb(0,0,0)" >f1</text>
diff --git a/tests/fc_script/for-list-functions.h b/tests/fc_script/for-list-functions.h
deleted file mode 100644
index 5bafea75c4645ebf8dc819c9ddee29931891d2cf..0000000000000000000000000000000000000000
--- a/tests/fc_script/for-list-functions.h
+++ /dev/null
@@ -1 +0,0 @@
-#include "for-list-functions2.h"
diff --git a/tests/fc_script/recursions.i b/tests/fc_script/heuristic-detect-recursion.t/heuristic-detect-recursion.i
similarity index 74%
rename from tests/fc_script/recursions.i
rename to tests/fc_script/heuristic-detect-recursion.t/heuristic-detect-recursion.i
index 77b0c7b1f57f26c28afe626abcbef7d3308b37dc..d65e2f474581d2ddd580f9d34b9f05b9812a449e 100644
--- a/tests/fc_script/recursions.i
+++ b/tests/fc_script/heuristic-detect-recursion.t/heuristic-detect-recursion.i
@@ -1,8 +1,3 @@
-/* run.config
- NOFRAMAC: testing frama-c-script, not frama-c itself
- EXECNOW: LOG recursions.res LOG recursions.err PTESTS_TESTING=1 %{bin:frama-c-script} heuristic-detect-recursion @PTEST_FILE@ > ./recursions.res 2> ./recursions.err
-*/
-
volatile int v;
void g() {
diff --git a/tests/fc_script/heuristic-detect-recursion.t/run.t b/tests/fc_script/heuristic-detect-recursion.t/run.t
new file mode 100644
index 0000000000000000000000000000000000000000..e483cc8930d08a4295197b3469cd38193c964bd0
--- /dev/null
+++ b/tests/fc_script/heuristic-detect-recursion.t/run.t
@@ -0,0 +1,19 @@
+ $ PTESTS_TESTING=1 frama-c-script heuristic-detect-recursion heuristic-detect-recursion.i
+ recursive cycle detected:
+ heuristic-detect-recursion.i:44: direct_rec -> direct_rec
+ recursive cycle detected:
+ heuristic-detect-recursion.i:8: f -> f
+ recursive cycle detected:
+ heuristic-detect-recursion.i:13: h -> h
+ recursive cycle detected:
+ heuristic-detect-recursion.i:54: indirect_rec1 -> indirect_rec2
+ heuristic-detect-recursion.i:50: indirect_rec2 -> indirect_rec1
+ recursive cycle detected:
+ heuristic-detect-recursion.i:29: k -> l
+ heuristic-detect-recursion.i:33: l -> m
+ heuristic-detect-recursion.i:37: m -> k
+ recursive cycle detected:
+ heuristic-detect-recursion.i:69: multiple_indirect1 -> multiple_indirect2
+ heuristic-detect-recursion.i:70: multiple_indirect1 -> multiple_indirect2
+ heuristic-detect-recursion.i:64: multiple_indirect2 -> multiple_indirect1
+ heuristic-detect-recursion.i:65: multiple_indirect2 -> multiple_indirect1
diff --git a/tests/fc_script/heuristic-list-functions.t/build-callgraph.c b/tests/fc_script/heuristic-list-functions.t/build-callgraph.c
new file mode 100644
index 0000000000000000000000000000000000000000..1e235e1d4355bed11efafbe785fed75ae6fff39f
--- /dev/null
+++ b/tests/fc_script/heuristic-list-functions.t/build-callgraph.c
@@ -0,0 +1,64 @@
+#include <stdio.h>
+void main() {
+ strlen("");
+}
+struct s {
+ int a; int b;
+} s;
+
+volatile int v;
+
+int fn2(int, int);
+
+int fn1(int x, int y)
+{
+ Frama_C_show_each_1(x);
+ Frama_C_show_each_2(y);
+ return x + y;
+}
+
+int X, Y;
+int main1 () {
+ R1 = fn1(G, G|0);
+ R2 = fn2(G, G|0);
+ Frama_C_show_each_d(G);
+ pv = (int *) &X;
+ return Y;
+}
+
+int * main2() {
+ return 0;
+}
+
+#define not_a_function_call(v) \
+ yes_a_function_call(v)
+
+#define yet_another_not_a_call(v) do { \
+ yes_again(); \
+ } while (0)
+
+/* call_inside_comment(evaluation); */
+void main3 () {
+ //@ not_a_function_call(v);
+ yet_another_not_a_call(v);
+}
+
+/* Tests the initialization of local variables. */
+void main4 () {
+ f(g(h(i, j), k (l, m ( n(
+ o, p(
+ q)
+ )
+ )
+ )
+ )
+ );
+ f();
+ g();
+}
+void main() {
+ main1();
+ main2();
+ main3();
+ main4();
+}
diff --git a/tests/fc_script/heuristic-list-functions.t/find-fun.c b/tests/fc_script/heuristic-list-functions.t/find-fun.c
new file mode 100644
index 0000000000000000000000000000000000000000..2e7404d8bb4a24feaa072e5088e4806aa5402168
--- /dev/null
+++ b/tests/fc_script/heuristic-list-functions.t/find-fun.c
@@ -0,0 +1,13 @@
+int
+main2
+(char *c, int i);
+
+struct s {
+ char c;
+};
+
+struct s **main3(
+ struct s *p1, struct s s2
+ ) {
+
+}
diff --git a/tests/fc_script/heuristic-list-functions.t/find-fun2.c b/tests/fc_script/heuristic-list-functions.t/find-fun2.c
new file mode 100644
index 0000000000000000000000000000000000000000..9bf89918db1f250310a2357de6e0cc7133c15e82
--- /dev/null
+++ b/tests/fc_script/heuristic-list-functions.t/find-fun2.c
@@ -0,0 +1,27 @@
+struct s ** main3(
+ struct s *p1, struct s s2
+ ) ;
+
+// tests to avoid false positives
+void f() {
+ int (*false_positive)();
+}
+
+void g() {
+ int i = 0;
+ false_positive(i);
+}
+
+void h() {
+ (void)false_positive((int)42);
+}
+
+//void false_positive();
+
+ void false_positive(); // this is a "voluntary" false negative (space before):
+ // it allows us to avoid false positives more easily
+
+static int static_fun() {
+ static int init = 0;
+ return init;
+}
diff --git a/tests/fc_script/heuristic-list-functions.t/heuristic-detect-recursion.i b/tests/fc_script/heuristic-list-functions.t/heuristic-detect-recursion.i
new file mode 100644
index 0000000000000000000000000000000000000000..d65e2f474581d2ddd580f9d34b9f05b9812a449e
--- /dev/null
+++ b/tests/fc_script/heuristic-list-functions.t/heuristic-detect-recursion.i
@@ -0,0 +1,71 @@
+volatile int v;
+
+void g() {
+ int g = 42;
+}
+
+void f() {
+ if (v) f();
+ else g();
+}
+
+void h() {
+ if (v) h();
+ else g();
+}
+
+void i() {
+ g();
+}
+
+void j() {
+ f();
+}
+
+void l(void);
+void m(void);
+
+void k() {
+ if (v) l();
+}
+
+void l() {
+ if (v) m();
+}
+
+void m() {
+ if (v) k();
+}
+
+void norec() {
+}
+
+int direct_rec() {
+ return direct_rec();
+}
+
+void indirect_rec1();
+
+void indirect_rec2() {
+ indirect_rec1();
+}
+
+void indirect_rec1() {
+ indirect_rec2();
+}
+
+void decl_only();
+
+void one_liner_function() { decl_only(); }
+
+void multiple_indirect1();
+
+void multiple_indirect2() {
+ multiple_indirect1();
+ multiple_indirect1();
+}
+
+void multiple_indirect1() {
+ multiple_indirect2();
+ multiple_indirect2();
+}
diff --git a/tests/fc_script/heuristic-list-functions.t/list-functions.c b/tests/fc_script/heuristic-list-functions.t/list-functions.c
new file mode 100644
index 0000000000000000000000000000000000000000..a71c42a5419902342063bc2823348d09edf00df9
--- /dev/null
+++ b/tests/fc_script/heuristic-list-functions.t/list-functions.c
@@ -0,0 +1,18 @@
+#include "list-functions2.h"
+#include "list-functions.h"
+
+static int static_fun() {
+ static int init = 0;
+ if (!init) {
+ init = 1;
+ return 2;
+ }
+ return 4;
+}
+
+void k() {
+ /*@ loop unroll 10; */ // Eva is not loaded, so we must ignore the annotation
+ for (int i = 0; i < 10; i++) {
+ extf();
+ }
+}
diff --git a/tests/fc_script/heuristic-list-functions.t/list-functions.h b/tests/fc_script/heuristic-list-functions.t/list-functions.h
new file mode 100644
index 0000000000000000000000000000000000000000..03dc1c5a66c5922de1a77aa7062da9137e21a960
--- /dev/null
+++ b/tests/fc_script/heuristic-list-functions.t/list-functions.h
@@ -0,0 +1 @@
+#include "list-functions2.h"
diff --git a/tests/fc_script/for-list-functions2.h b/tests/fc_script/heuristic-list-functions.t/list-functions2.h
similarity index 100%
rename from tests/fc_script/for-list-functions2.h
rename to tests/fc_script/heuristic-list-functions.t/list-functions2.h
diff --git a/tests/fc_script/heuristic-list-functions.t/main.c b/tests/fc_script/heuristic-list-functions.t/main.c
new file mode 100644
index 0000000000000000000000000000000000000000..153f05566005b05b8f14e36024a18fef0be1327b
--- /dev/null
+++ b/tests/fc_script/heuristic-list-functions.t/main.c
@@ -0,0 +1,3 @@
+void main() {
+
+}
diff --git a/tests/fc_script/heuristic-list-functions.t/main2.c b/tests/fc_script/heuristic-list-functions.t/main2.c
new file mode 100644
index 0000000000000000000000000000000000000000..1112eff2ded306e8f3248bd30f997464ed430a15
--- /dev/null
+++ b/tests/fc_script/heuristic-list-functions.t/main2.c
@@ -0,0 +1,11 @@
+void fake_main() {
+
+}
+
+void domain() {
+
+}
+
+void main2() {
+
+}
diff --git a/tests/fc_script/heuristic-list-functions.t/main3.c b/tests/fc_script/heuristic-list-functions.t/main3.c
new file mode 100644
index 0000000000000000000000000000000000000000..fc9ce92c7d7c43c39dd1f7b6acaeaa2afd3f0706
--- /dev/null
+++ b/tests/fc_script/heuristic-list-functions.t/main3.c
@@ -0,0 +1,4 @@
+int main( int argc, char *argv[] )
+{
+
+}
diff --git a/tests/fc_script/heuristic-list-functions.t/make-wrapper.c b/tests/fc_script/heuristic-list-functions.t/make-wrapper.c
new file mode 100644
index 0000000000000000000000000000000000000000..61fd6c259a1d7c85b7f0f475ba1df5b92eadf73b
--- /dev/null
+++ b/tests/fc_script/heuristic-list-functions.t/make-wrapper.c
@@ -0,0 +1,21 @@
+int defined(int a);
+
+int specified(int a);
+
+int external(int a);
+
+int large_name_to_force_line_break_in_stack_msg(void) {
+ return large_name_to_force_line_break_in_stack_msg();
+}
+
+int rec(void) {
+ return large_name_to_force_line_break_in_stack_msg();
+}
+
+int main() {
+ int a = 42;
+ a = rec();
+ a = defined(a);
+ a = specified(a);
+ a = external(a);
+}
diff --git a/tests/fc_script/heuristic-list-functions.t/make-wrapper2.c b/tests/fc_script/heuristic-list-functions.t/make-wrapper2.c
new file mode 100644
index 0000000000000000000000000000000000000000..443b405d3cf6ab856ad9cba55b9d17aec938d44e
--- /dev/null
+++ b/tests/fc_script/heuristic-list-functions.t/make-wrapper2.c
@@ -0,0 +1,12 @@
+int defined(int a) {
+ return a + 1;
+}
+
+/*@
+ assigns \result \from a;
+ ensures \result == a + 2;
+ */
+int specified(int a);
+
+// defined in another, non-included, file
+int external(int a);
diff --git a/tests/fc_script/heuristic-list-functions.t/make-wrapper3.c b/tests/fc_script/heuristic-list-functions.t/make-wrapper3.c
new file mode 100644
index 0000000000000000000000000000000000000000..9e04031a275ed6dd6a4268d47a79b42ef0ea021f
--- /dev/null
+++ b/tests/fc_script/heuristic-list-functions.t/make-wrapper3.c
@@ -0,0 +1,5 @@
+// This file contains a definition for function 'external', but it is _not_
+// included when parsing 'make-wrapper.c'. This triggers a make-wrapper message.
+int external(int a) {
+ return a + 3;
+}
diff --git a/tests/fc_script/heuristic-list-functions.t/run.t b/tests/fc_script/heuristic-list-functions.t/run.t
new file mode 100644
index 0000000000000000000000000000000000000000..a83608af084e739327a230d5429492c20c3b19a4
--- /dev/null
+++ b/tests/fc_script/heuristic-list-functions.t/run.t
@@ -0,0 +1,53 @@
+ $ frama-c-script heuristic-list-functions true true *.c *.i
+ build-callgraph.c:2:4: main (definition)
+ build-callgraph.c:11:11: fn2 (declaration)
+ build-callgraph.c:13:18: fn1 (definition)
+ build-callgraph.c:21:27: main1 (definition)
+ build-callgraph.c:29:31: main2 (definition)
+ build-callgraph.c:41:44: main3 (definition)
+ build-callgraph.c:47:58: main4 (definition)
+ build-callgraph.c:59:64: main (definition)
+ find-fun.c:2:3: main2 (declaration)
+ find-fun.c:9:13: main3 (definition)
+ find-fun2.c:1:3: main3 (declaration)
+ find-fun2.c:6:8: f (definition)
+ find-fun2.c:10:13: g (definition)
+ find-fun2.c:15:17: h (definition)
+ find-fun2.c:24:27: static_fun (definition)
+ list-functions.c:4:11: static_fun (definition)
+ list-functions.c:13:18: k (definition)
+ main.c:1:3: main (definition)
+ main2.c:1:3: fake_main (definition)
+ main2.c:5:7: domain (definition)
+ main2.c:9:11: main2 (definition)
+ main3.c:1:4: main (definition)
+ make-wrapper.c:1:1: defined (declaration)
+ make-wrapper.c:3:3: specified (declaration)
+ make-wrapper.c:5:5: external (declaration)
+ make-wrapper.c:7:9: large_name_to_force_line_break_in_stack_msg (definition)
+ make-wrapper.c:11:13: rec (definition)
+ make-wrapper.c:15:21: main (definition)
+ make-wrapper2.c:1:3: defined (definition)
+ make-wrapper2.c:9:9: specified (declaration)
+ make-wrapper2.c:12:12: external (declaration)
+ make-wrapper3.c:3:5: external (definition)
+ heuristic-detect-recursion.i:3:5: g (definition)
+ heuristic-detect-recursion.i:7:10: f (definition)
+ heuristic-detect-recursion.i:12:15: h (definition)
+ heuristic-detect-recursion.i:17:19: i (definition)
+ heuristic-detect-recursion.i:21:23: j (definition)
+ heuristic-detect-recursion.i:25:25: l (declaration)
+ heuristic-detect-recursion.i:26:26: m (declaration)
+ heuristic-detect-recursion.i:28:30: k (definition)
+ heuristic-detect-recursion.i:32:34: l (definition)
+ heuristic-detect-recursion.i:36:38: m (definition)
+ heuristic-detect-recursion.i:40:41: norec (definition)
+ heuristic-detect-recursion.i:43:45: direct_rec (definition)
+ heuristic-detect-recursion.i:47:47: indirect_rec1 (declaration)
+ heuristic-detect-recursion.i:49:51: indirect_rec2 (definition)
+ heuristic-detect-recursion.i:53:55: indirect_rec1 (definition)
+ heuristic-detect-recursion.i:57:57: decl_only (declaration)
+ heuristic-detect-recursion.i:59:59: one_liner_function (definition)
+ heuristic-detect-recursion.i:61:61: multiple_indirect1 (declaration)
+ heuristic-detect-recursion.i:63:66: multiple_indirect2 (definition)
+ heuristic-detect-recursion.i:68:71: multiple_indirect1 (definition)
diff --git a/tests/fc_script/list_files.json b/tests/fc_script/list-files.t/compile_commands.json
similarity index 77%
rename from tests/fc_script/list_files.json
rename to tests/fc_script/list-files.t/compile_commands.json
index d3ab75506354c08d7b4a39de880f5d05588a8ea2..8fd61f21fdfe1f72df5aaf08a9728e905c66b2af 100644
--- a/tests/fc_script/list_files.json
+++ b/tests/fc_script/list-files.t/compile_commands.json
@@ -14,5 +14,9 @@
{ "directory": ".",
"command": "gcc",
"file": "main3.c"
+ },
+ { "directory": ".",
+ "command": "gcc",
+ "file": "does_not_exist.c"
}
]
diff --git a/tests/fc_script/list-files.t/main.c b/tests/fc_script/list-files.t/main.c
new file mode 100644
index 0000000000000000000000000000000000000000..153f05566005b05b8f14e36024a18fef0be1327b
--- /dev/null
+++ b/tests/fc_script/list-files.t/main.c
@@ -0,0 +1,3 @@
+void main() {
+
+}
diff --git a/tests/fc_script/list-files.t/main2.c b/tests/fc_script/list-files.t/main2.c
new file mode 100644
index 0000000000000000000000000000000000000000..1112eff2ded306e8f3248bd30f997464ed430a15
--- /dev/null
+++ b/tests/fc_script/list-files.t/main2.c
@@ -0,0 +1,11 @@
+void fake_main() {
+
+}
+
+void domain() {
+
+}
+
+void main2() {
+
+}
diff --git a/tests/fc_script/list-files.t/main3.c b/tests/fc_script/list-files.t/main3.c
new file mode 100644
index 0000000000000000000000000000000000000000..fc9ce92c7d7c43c39dd1f7b6acaeaa2afd3f0706
--- /dev/null
+++ b/tests/fc_script/list-files.t/main3.c
@@ -0,0 +1,4 @@
+int main( int argc, char *argv[] )
+{
+
+}
diff --git a/tests/fc_script/list-files.t/run.t b/tests/fc_script/list-files.t/run.t
new file mode 100644
index 0000000000000000000000000000000000000000..ea07d724a71c1d09d16033485f19b55dc21977ce
--- /dev/null
+++ b/tests/fc_script/list-files.t/run.t
@@ -0,0 +1,13 @@
+ $ frama-c-script list-files
+ # Paths as seen by a makefile inside subdirectory '.frama-c':
+ SRCS=\
+ ../does_not_exist.c \
+ ../main.c \
+ ../main2.c \
+ ../main3.c \
+
+ warning: could not read file 'does_not_exist.c', mentioned in 'compile_commands.json'. Skipping check of 'main' function.
+
+ # Possible definition of main function in the following file(s), as seen from '.frama-c':
+ ../main.c
+ ../main3.c
diff --git a/tests/fc_script/list-functions.t/find-fun2.c b/tests/fc_script/list-functions.t/find-fun2.c
new file mode 100644
index 0000000000000000000000000000000000000000..9bf89918db1f250310a2357de6e0cc7133c15e82
--- /dev/null
+++ b/tests/fc_script/list-functions.t/find-fun2.c
@@ -0,0 +1,27 @@
+struct s ** main3(
+ struct s *p1, struct s s2
+ ) ;
+
+// tests to avoid false positives
+void f() {
+ int (*false_positive)();
+}
+
+void g() {
+ int i = 0;
+ false_positive(i);
+}
+
+void h() {
+ (void)false_positive((int)42);
+}
+
+//void false_positive();
+
+ void false_positive(); // this is a "voluntary" false negative (space before):
+ // it allows us to avoid false positives more easily
+
+static int static_fun() {
+ static int init = 0;
+ return init;
+}
diff --git a/tests/fc_script/list-functions.t/list-functions.c b/tests/fc_script/list-functions.t/list-functions.c
new file mode 100644
index 0000000000000000000000000000000000000000..a71c42a5419902342063bc2823348d09edf00df9
--- /dev/null
+++ b/tests/fc_script/list-functions.t/list-functions.c
@@ -0,0 +1,18 @@
+#include "list-functions2.h"
+#include "list-functions.h"
+
+static int static_fun() {
+ static int init = 0;
+ if (!init) {
+ init = 1;
+ return 2;
+ }
+ return 4;
+}
+
+void k() {
+ /*@ loop unroll 10; */ // Eva is not loaded, so we must ignore the annotation
+ for (int i = 0; i < 10; i++) {
+ extf();
+ }
+}
diff --git a/tests/fc_script/list-functions.t/list-functions.h b/tests/fc_script/list-functions.t/list-functions.h
new file mode 100644
index 0000000000000000000000000000000000000000..03dc1c5a66c5922de1a77aa7062da9137e21a960
--- /dev/null
+++ b/tests/fc_script/list-functions.t/list-functions.h
@@ -0,0 +1 @@
+#include "list-functions2.h"
diff --git a/tests/fc_script/list-functions.t/list-functions2.h b/tests/fc_script/list-functions.t/list-functions2.h
new file mode 100644
index 0000000000000000000000000000000000000000..7338669a3ed39623e9a31ad38ce5716178fcfd5f
--- /dev/null
+++ b/tests/fc_script/list-functions.t/list-functions2.h
@@ -0,0 +1 @@
+extern void extf(void);
diff --git a/tests/fc_script/list-functions.t/run.t b/tests/fc_script/list-functions.t/run.t
new file mode 100644
index 0000000000000000000000000000000000000000..c60ff95542d9edadbeb104ec3bbee06c93cf3765
--- /dev/null
+++ b/tests/fc_script/list-functions.t/run.t
@@ -0,0 +1,26 @@
+ $ frama-c-script list-functions find-fun2.c list-functions.c
+ [kernel:typing:implicit-function-declaration] find-fun2.c:12: Warning:
+ Calling undeclared function false_positive. Old style K&R code?
+ f: defined at find-fun2.c:6 (1 statement);
+ g: defined at find-fun2.c:10 (3 statements);
+ h: defined at find-fun2.c:15 (2 statements);
+ k: defined at list-functions.c:13 (8 statements);
+ static_fun: defined at find-fun2.c:24 (1 statement), list-functions.c:4 (7 statements);
+
+ $ frama-c-script list-functions find-fun2.c list-functions.c -list-functions-declarations -list-functions-output ./list-functions2.json -list-functions-debug 1
+ [kernel:typing:implicit-function-declaration] find-fun2.c:12: Warning:
+ Calling undeclared function false_positive. Old style K&R code?
+ [list-functions] List written to: list-functions2.json
+
+ $ cat list-functions2.json
+ [ { "extf": { "declarations": [ "list-functions2.h:1" ] } },
+ { "f": { "definitions": [ { "location": "find-fun2.c:6", "statements": 1 } ] } },
+ { "false_positive": { "declarations": [ "find-fun2.c:21" ] } },
+ { "g": { "definitions": [ { "location": "find-fun2.c:10", "statements": 3 } ] } },
+ { "h": { "definitions": [ { "location": "find-fun2.c:15", "statements": 2 } ] } },
+ { "k": { "definitions": [ { "location": "list-functions.c:13",
+ "statements": 8 } ] } },
+ { "static_fun": { "definitions": [ { "location": "find-fun2.c:24",
+ "statements": 1 },
+ { "location": "list-functions.c:4",
+ "statements": 7 } ] } } ]
diff --git a/tests/fc_script/list_functions.i b/tests/fc_script/list_functions.i
deleted file mode 100644
index 75e20a87360c92e2e5b3f47155b2fb53e64762b4..0000000000000000000000000000000000000000
--- a/tests/fc_script/list_functions.i
+++ /dev/null
@@ -1,19 +0,0 @@
-/* run.config
- NOFRAMAC: testing frama-c-script, not frama-c itself
-
- DEPS: @PTEST_DEPS@ ./for-find-fun.c
- DEPS: @PTEST_DEPS@ ./for-find-fun2.c
- DEPS: @PTEST_DEPS@ ./for-list-functions.c
- DEPS: @PTEST_DEPS@ ./list_functions.i
- DEPS: @PTEST_DEPS@ ./main.c
- DEPS: @PTEST_DEPS@ ./main2.c
- DEPS: @PTEST_DEPS@ ./main3.c
- DEPS: @PTEST_DEPS@ ./make-wrapper.c
- DEPS: @PTEST_DEPS@ ./make-wrapper2.c
- DEPS: @PTEST_DEPS@ ./make-wrapper3.c
-
- DEPS: @PTEST_DEPS@ ./build-callgraph.i
- DEPS: @PTEST_DEPS@ ./recursions.i
-
- EXECNOW: LOG heuristic_list_functions.res LOG heuristic_list_functions.err PTESTS_TESTING=1 %{bin:frama-c-script} heuristic-list-functions true true @PTEST_DEPS@ > ./heuristic_list_functions.res 2> ./heuristic_list_functions.err
- */
diff --git a/tests/fc_script/main.c b/tests/fc_script/main.c
deleted file mode 100644
index 7a490e293ff63380fa3ee3e017ccd74713fa4aeb..0000000000000000000000000000000000000000
--- a/tests/fc_script/main.c
+++ /dev/null
@@ -1,20 +0,0 @@
-/* run.config
- NOFRAMAC: testing frama-c-script, not frama-c itself
- COMMENT: the 'build' command cannot be tested because it requires 'glub'.
- DEPS: main2.c main3.c main.c
- EXECNOW: LOG list_files.res LOG list_files.err PTESTS_TESTING=1 %{bin:frama-c-script} list-files %{dep:./list_files.json} > ./list_files.res 2> ./list_files.err
- DEPS: build-callgraph.i estimate_difficulty.i for-find-fun2.c for-find-fun.c for-list-functions.c for-list-functions.h for-list-functions2.h list_functions.i main2.c main3.c main.c make-wrapper2.c make-wrapper3.c make-wrapper.c recursions.i
- EXECNOW: LOG find_fun1.res LOG find_fun1.err PTESTS_TESTING=1 %{bin:frama-c-script} find-fun main2 ./ > ./find_fun1.res 2> ./find_fun1.err
- EXECNOW: LOG find_fun2.res LOG find_fun2.err PTESTS_TESTING=1 %{bin:frama-c-script} find-fun main3 ./ > ./find_fun2.res 2> ./find_fun2.err
- EXECNOW: LOG find_fun3.res LOG find_fun3.err PTESTS_TESTING=1 %{bin:frama-c-script} find-fun false_positive ./ > ./find_fun3.res 2> ./find_fun3.err
- DEPS:
- EXECNOW: LOG list_functions.res LOG list_functions.err PTESTS_TESTING=1 %{bin:frama-c-script} list-functions %{dep:./for-find-fun2.c} %{dep:./for-list-functions.c} > ./list_functions.res 2> ./list_functions.err
- EXECNOW: LOG list_functions2.res LOG list_functions2.err LOG list_functions2.json PTESTS_TESTING=1 %{bin:frama-c-script} list-functions %{dep:./for-find-fun2.c} %{dep:./for-list-functions.c} -list-functions-declarations -list-functions-output ./list_functions2.json -list-functions-debug 1 > ./list_functions2.res 2> ./list_functions2.err
- */
-
-
-
-void main() {
-
-}
-// NB: Dependency to ./share directory where are script files used by %{bin:frama-c-script} is implicit with `dune` testing.
diff --git a/tests/fc_script/main3.c b/tests/fc_script/main3.c
deleted file mode 100644
index c1b7c0f74308d656e5cd6c1c200370b500c4eb72..0000000000000000000000000000000000000000
--- a/tests/fc_script/main3.c
+++ /dev/null
@@ -1,9 +0,0 @@
-/* run.config
- DONTRUN:
- COMMENT: used by main.c
- */
-
-int main( int argc, char *argv[] )
-{
-
-}
diff --git a/tests/fc_script/make-machdep.t/run.t b/tests/fc_script/make-machdep.t/run.t
new file mode 100644
index 0000000000000000000000000000000000000000..917e6c88d2ef9ccb4e6ea22f3b2fc30f66c575c7
--- /dev/null
+++ b/tests/fc_script/make-machdep.t/run.t
@@ -0,0 +1,184 @@
+ $ frama-c-script make-machdep --compiler clang --cpp-arch-flags='--target=x86_64' | yq -Y 'del(.version)|del(.custom_defs)'
+ alignof_aligned: 16
+ alignof_double: 8
+ alignof_float: 4
+ alignof_fun: 4
+ alignof_int: 4
+ alignof_long: 8
+ alignof_longdouble: 16
+ alignof_longlong: 8
+ alignof_ptr: 8
+ alignof_short: 2
+ alignof_str: 1
+ bufsiz: '8192'
+ char_is_unsigned: false
+ compiler: clang
+ cpp_arch_flags:
+ - --target=x86_64
+ eof: (-1)
+ errno:
+ e2big: '7'
+ eacces: '13'
+ eaddrinuse: '98'
+ eaddrnotavail: '99'
+ eafnosupport: '97'
+ eagain: '11'
+ ealready: '114'
+ ebade: '52'
+ ebadf: '9'
+ ebadfd: '77'
+ ebadmsg: '74'
+ ebadr: '53'
+ ebadrqc: '56'
+ ebadslt: '57'
+ ebusy: '16'
+ ecanceled: '125'
+ echild: '10'
+ echrng: '44'
+ ecomm: '70'
+ econnaborted: '103'
+ econnrefused: '111'
+ econnreset: '104'
+ edeadlk: '35'
+ edeadlock: '35'
+ edestaddrreq: '89'
+ edom: '33'
+ edquot: '122'
+ eexist: '17'
+ efault: '14'
+ efbig: '27'
+ ehostdown: '112'
+ ehostunreach: '113'
+ eidrm: '43'
+ eilseq: '84'
+ einprogress: '115'
+ eintr: '4'
+ einval: '22'
+ eio: '5'
+ eisconn: '106'
+ eisdir: '21'
+ eisnam: '120'
+ ekeyexpired: '127'
+ ekeyrejected: '129'
+ ekeyrevoked: '128'
+ el2hlt: '51'
+ el2nsync: '45'
+ el3hlt: '46'
+ el3rst: '47'
+ elibacc: '79'
+ elibbad: '80'
+ elibexec: '83'
+ elibmax: '82'
+ elibscn: '81'
+ eloop: '40'
+ emediumtype: '124'
+ emfile: '24'
+ emlink: '31'
+ emsgsize: '90'
+ emultihop: '72'
+ enametoolong: '36'
+ enetdown: '100'
+ enetreset: '102'
+ enetunreach: '101'
+ enfile: '23'
+ enobufs: '105'
+ enodata: '61'
+ enodev: '19'
+ enoent: '2'
+ enoexec: '8'
+ enokey: '126'
+ enolck: '37'
+ enolink: '67'
+ enomedium: '123'
+ enomem: '12'
+ enomsg: '42'
+ enonet: '64'
+ enopkg: '65'
+ enoprotoopt: '92'
+ enospc: '28'
+ enosr: '63'
+ enostr: '60'
+ enosys: '38'
+ enotblk: '15'
+ enotconn: '107'
+ enotdir: '20'
+ enotempty: '39'
+ enotrecoverable: '131'
+ enotsock: '88'
+ enotsup: '95'
+ enotty: '25'
+ enotuniq: '76'
+ enxio: '6'
+ eopnotsupp: '95'
+ eoverflow: '75'
+ eownerdead: '130'
+ eperm: '1'
+ epfnosupport: '96'
+ epipe: '32'
+ eproto: '71'
+ eprotonosupport: '93'
+ eprototype: '91'
+ erange: '34'
+ eremchg: '78'
+ eremote: '66'
+ eremoteio: '121'
+ erestart: '85'
+ erofs: '30'
+ eshutdown: '108'
+ esocktnosupport: '94'
+ espipe: '29'
+ esrch: '3'
+ estale: '116'
+ estrpipe: '86'
+ etime: '62'
+ etimedout: '110'
+ etxtbsy: '26'
+ euclean: '117'
+ eunatch: '49'
+ eusers: '87'
+ ewouldblock: '11'
+ exdev: '18'
+ exfull: '54'
+ filename_max: '4096'
+ fopen_max: '16'
+ has__builtin_va_list: true
+ host_name_max: '64'
+ int_fast16_t: long
+ int_fast32_t: long
+ int_fast64_t: long
+ int_fast8_t: signed char
+ intptr_t: long
+ l_tmpnam: '20'
+ little_endian: true
+ machdep_name: anonymous_machdep
+ mb_cur_max: ((size_t)16)
+ nsig: (64 + 1)
+ path_max: '4096'
+ posix_version: 200809L
+ ptrdiff_t: long
+ rand_max: '2147483647'
+ sig_atomic_t: int
+ size_t: unsigned long
+ sizeof_double: 8
+ sizeof_float: 4
+ sizeof_fun: 1
+ sizeof_int: 4
+ sizeof_long: 8
+ sizeof_longdouble: 16
+ sizeof_longlong: 8
+ sizeof_ptr: 8
+ sizeof_short: 2
+ sizeof_void: 1
+ ssize_t: long
+ time_t: long
+ tmp_max: '238328'
+ tty_name_max: '32'
+ uint_fast16_t: unsigned long
+ uint_fast32_t: unsigned long
+ uint_fast64_t: unsigned long
+ uint_fast8_t: unsigned char
+ uintptr_t: unsigned long
+ wchar_t: int
+ weof: (0xffffffffu)
+ wint_t: int
+ wordsize: '64'
diff --git a/tests/fc_script/make-for-make-wrapper.mk b/tests/fc_script/make-wrapper.t/make-for-make-wrapper.mk
similarity index 77%
rename from tests/fc_script/make-for-make-wrapper.mk
rename to tests/fc_script/make-wrapper.t/make-for-make-wrapper.mk
index 5cac4969ff81cf3cbc03f8a4bdab0c78178237ee..84b0478b0b5f0f255537cdd8de2288072c4e06f9 100644
--- a/tests/fc_script/make-for-make-wrapper.mk
+++ b/tests/fc_script/make-wrapper.t/make-for-make-wrapper.mk
@@ -1,6 +1,6 @@
# Customized makefile template for testing 'frama-c-script make-wrapper'.
-include $(shell $(FRAMAC) -no-autoload-plugins -print-lib-path)/analysis-scripts/prologue.mk
+include $(shell frama-c-config -print-lib-path)/analysis-scripts/prologue.mk
FCFLAGS += \
-kernel-warn-key annot:missing-spec=abort \
@@ -18,5 +18,5 @@ make-for-make-wrapper.parse: \
# make-wrapper3.c is deliberately absent of this list
### Epilogue. Do not modify this block. #######################################
-include $(shell $(FRAMAC) -no-autoload-plugins -print-lib-path)/analysis-scripts/epilogue.mk
+include $(shell frama-c-config -print-lib-path)/analysis-scripts/epilogue.mk
###############################################################################
diff --git a/tests/fc_script/make-wrapper.c b/tests/fc_script/make-wrapper.t/make-wrapper.c
similarity index 100%
rename from tests/fc_script/make-wrapper.c
rename to tests/fc_script/make-wrapper.t/make-wrapper.c
diff --git a/tests/fc_script/make-wrapper2.c b/tests/fc_script/make-wrapper.t/make-wrapper2.c
similarity index 100%
rename from tests/fc_script/make-wrapper2.c
rename to tests/fc_script/make-wrapper.t/make-wrapper2.c
diff --git a/tests/fc_script/make-wrapper3.c b/tests/fc_script/make-wrapper.t/make-wrapper3.c
similarity index 100%
rename from tests/fc_script/make-wrapper3.c
rename to tests/fc_script/make-wrapper.t/make-wrapper3.c
diff --git a/tests/fc_script/make-wrapper.t/run.t b/tests/fc_script/make-wrapper.t/run.t
new file mode 100644
index 0000000000000000000000000000000000000000..3357049cef462d44d7f99c14ca385a21fa8448dc
--- /dev/null
+++ b/tests/fc_script/make-wrapper.t/run.t
@@ -0,0 +1,51 @@
+First we 'touch' the files to update their timestamp, so that the 'make'
+command will re-run the analysis
+ $ touch make-wrapper2.c make-wrapper3.c
+
+In case of errors, consider removing the '-s' option below to get a more
+verbose output for Make.
+ $ PTESTS_TESTING=1 frama-c-script make-wrapper --make-dir . -f make-for-make-wrapper.mk -s
+
+ Command: frama-c -kernel-warn-key annot:missing-spec=abort -kernel-warn-key typing:implicit-function-declaration=abort -cpp-extra-args= make-wrapper.c make-wrapper2.c
+
+ [kernel] Parsing make-wrapper.c (with preprocessing)
+ [kernel] Parsing make-wrapper2.c (with preprocessing)
+
+ Command: frama-c -kernel-warn-key annot:missing-spec=abort -kernel-warn-key typing:implicit-function-declaration=abort -eva -eva-no-print -eva-no-show-progress -eva-msg-key=-initial-state -eva-print-callstacks -eva-warn-key alarm=inactive -no-deps-print -no-calldeps-print -eva-warn-key garbled-mix -calldeps -from-verbose 0 -eva-warn-key builtins:missing-spec=abort
+
+ [eva] Analyzing a complete application starting at main
+ [eva:recursion] make-wrapper.c:17:
+ detected recursive call
+ of function large_name_to_force_line_break_in_stack_msg.
+ [eva] make-wrapper.c:17: User Error:
+ Recursive call to large_name_to_force_line_break_in_stack_msg
+ without assigns clause.
+ Generating probably incomplete assigns to interpret the call. Try to increase
+ the -eva-unroll-recursive-calls parameter or write a correct specification
+ for function large_name_to_force_line_break_in_stack_msg.
+ stack: large_name_to_force_line_break_in_stack_msg :: make-wrapper.c:17 <-
+ large_name_to_force_line_break_in_stack_msg :: make-wrapper.c:21 <-
+ rec :: make-wrapper.c:26 <-
+ main
+ [kernel:annot:missing-spec] make-wrapper.c:16: Warning:
+ Neither code nor specification for function large_name_to_force_line_break_in_stack_msg, generating default assigns from the prototype
+ [kernel] User Error: warning annot:missing-spec treated as fatal error.
+ [kernel] Frama-C aborted: invalid user input.
+
+ ***** make-wrapper recommendations *****
+
+ *** recommendation #1 ***
+
+ 1. Found recursive call at:
+ stack: large_name_to_force_line_break_in_stack_msg :: make-wrapper.c:17 <-
+ large_name_to_force_line_break_in_stack_msg :: make-wrapper.c:21 <-
+ rec :: make-wrapper.c:26 <-
+ main
+
+ Consider patching, stubbing or adding an ACSL specification to the recursive call, then re-run the analysis.
+
+ *** recommendation #2 ***
+ 2. Found function with missing specification: large_name_to_force_line_break_in_stack_msg
+ Looking for files defining it...
+ Add the following file to the list of sources to be parsed:
+ make-wrapper.c
diff --git a/tests/fc_script/oracle/GNUmakefile b/tests/fc_script/oracle/GNUmakefile
deleted file mode 100644
index 5cda2a5d946cf8a1b69fb364326b047eac15a460..0000000000000000000000000000000000000000
--- a/tests/fc_script/oracle/GNUmakefile
+++ /dev/null
@@ -1,55 +0,0 @@
-# Makefile template for Frama-C/Eva case studies.
-# For details and usage information, see the Frama-C User Manual.
-
-### Prologue. Do not modify this block. #######################################
--include path.mk # path.mk contains variables specific to each user
- # (e.g. FRAMAC, FRAMAC_GUI) and should not be versioned. It is
- # an optional include, unnecessary if frama-c is in the PATH.
-FRAMAC ?= frama-c # FRAMAC is defined in path.mk when it is included, but the
- # user can override it in the command-line.
-ifeq ($(FRAMAC_LIB),)
- FRAMAC_LIB := $(shell $(FRAMAC)-config -print-lib-path)
-endif
-include $(FRAMAC_LIB)/analysis-scripts/prologue.mk
-###############################################################################
-
-# Edit below as needed. Suggested flags are optional.
-
-MACHDEP = x86_64
-
-## Preprocessing flags (for -cpp-extra-args)
-CPPFLAGS += \
-
-## General flags
-FCFLAGS += \
- -json-compilation-database ./compile_commands.json \
- -main eva_main \
- -add-symbolic-path=.:. \
- -kernel-warn-key annot:missing-spec=abort \
- -kernel-warn-key typing:implicit-function-declaration=abort \
-
-## Eva-specific flags
-EVAFLAGS += \
- -eva-warn-key builtins:missing-spec=abort \
-
-## WP-specific flags
-WPFLAGS += \
-
-## GUI-only flags
-FCGUIFLAGS += \
-
-## Analysis targets (suffixed with .eva)
-TARGETS = fc_script_main.eva
-
-### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
-fc_script_main.parse: \
- fc_stubs.c \
- ./for-find-fun.c \
- ./for-find-fun2.c \
- ./main.c \
- ./main2.c \
- ./main3.c \
-
-### Epilogue. Do not modify this block. #######################################
-include $(FRAMAC_LIB)/analysis-scripts/epilogue.mk
-###############################################################################
diff --git a/tests/fc_script/oracle/build-callgraph.res b/tests/fc_script/oracle/build-callgraph.res
deleted file mode 100644
index 6d7c63756a39cdd917ba7795794b27d28c841877..0000000000000000000000000000000000000000
--- a/tests/fc_script/oracle/build-callgraph.res
+++ /dev/null
@@ -1,21 +0,0 @@
-build-callgraph.i:8: main -> strlen
-build-callgraph.i:20: fn1 -> Frama_C_show_each_1
-build-callgraph.i:21: fn1 -> Frama_C_show_each_2
-build-callgraph.i:27: main1 -> fn1
-build-callgraph.i:28: main1 -> fn2
-build-callgraph.i:29: main1 -> Frama_C_show_each_d
-build-callgraph.i:47: main3 -> not_a_function_call
-build-callgraph.i:48: main3 -> yet_another_not_a_call
-build-callgraph.i:53: main4 -> f
-build-callgraph.i:61: main4 -> f
-build-callgraph.i:53: main4 -> g
-build-callgraph.i:62: main4 -> g
-build-callgraph.i:53: main4 -> h
-build-callgraph.i:53: main4 -> k
-build-callgraph.i:53: main4 -> m
-build-callgraph.i:53: main4 -> n
-build-callgraph.i:54: main4 -> p
-build-callgraph.i:65: main -> main1
-build-callgraph.i:66: main -> main2
-build-callgraph.i:67: main -> main3
-build-callgraph.i:68: main -> main4
diff --git a/tests/fc_script/oracle/custom_machdep.yaml b/tests/fc_script/oracle/custom_machdep.yaml
deleted file mode 100644
index 24f472d19e21723c8f7bf328c8ff0a0bea41a373..0000000000000000000000000000000000000000
--- a/tests/fc_script/oracle/custom_machdep.yaml
+++ /dev/null
@@ -1,183 +0,0 @@
-alignof_aligned: 16
-alignof_double: 8
-alignof_float: 4
-alignof_fun: 4
-alignof_int: 4
-alignof_long: 8
-alignof_longdouble: 16
-alignof_longlong: 8
-alignof_ptr: 8
-alignof_short: 2
-alignof_str: 1
-bufsiz: '8192'
-char_is_unsigned: false
-compiler: clang
-cpp_arch_flags:
- - --target=x86_64
-eof: (-1)
-errno:
- e2big: '7'
- eacces: '13'
- eaddrinuse: '98'
- eaddrnotavail: '99'
- eafnosupport: '97'
- eagain: '11'
- ealready: '114'
- ebade: '52'
- ebadf: '9'
- ebadfd: '77'
- ebadmsg: '74'
- ebadr: '53'
- ebadrqc: '56'
- ebadslt: '57'
- ebusy: '16'
- ecanceled: '125'
- echild: '10'
- echrng: '44'
- ecomm: '70'
- econnaborted: '103'
- econnrefused: '111'
- econnreset: '104'
- edeadlk: '35'
- edeadlock: '35'
- edestaddrreq: '89'
- edom: '33'
- edquot: '122'
- eexist: '17'
- efault: '14'
- efbig: '27'
- ehostdown: '112'
- ehostunreach: '113'
- eidrm: '43'
- eilseq: '84'
- einprogress: '115'
- eintr: '4'
- einval: '22'
- eio: '5'
- eisconn: '106'
- eisdir: '21'
- eisnam: '120'
- ekeyexpired: '127'
- ekeyrejected: '129'
- ekeyrevoked: '128'
- el2hlt: '51'
- el2nsync: '45'
- el3hlt: '46'
- el3rst: '47'
- elibacc: '79'
- elibbad: '80'
- elibexec: '83'
- elibmax: '82'
- elibscn: '81'
- eloop: '40'
- emediumtype: '124'
- emfile: '24'
- emlink: '31'
- emsgsize: '90'
- emultihop: '72'
- enametoolong: '36'
- enetdown: '100'
- enetreset: '102'
- enetunreach: '101'
- enfile: '23'
- enobufs: '105'
- enodata: '61'
- enodev: '19'
- enoent: '2'
- enoexec: '8'
- enokey: '126'
- enolck: '37'
- enolink: '67'
- enomedium: '123'
- enomem: '12'
- enomsg: '42'
- enonet: '64'
- enopkg: '65'
- enoprotoopt: '92'
- enospc: '28'
- enosr: '63'
- enostr: '60'
- enosys: '38'
- enotblk: '15'
- enotconn: '107'
- enotdir: '20'
- enotempty: '39'
- enotrecoverable: '131'
- enotsock: '88'
- enotsup: '95'
- enotty: '25'
- enotuniq: '76'
- enxio: '6'
- eopnotsupp: '95'
- eoverflow: '75'
- eownerdead: '130'
- eperm: '1'
- epfnosupport: '96'
- epipe: '32'
- eproto: '71'
- eprotonosupport: '93'
- eprototype: '91'
- erange: '34'
- eremchg: '78'
- eremote: '66'
- eremoteio: '121'
- erestart: '85'
- erofs: '30'
- eshutdown: '108'
- esocktnosupport: '94'
- espipe: '29'
- esrch: '3'
- estale: '116'
- estrpipe: '86'
- etime: '62'
- etimedout: '110'
- etxtbsy: '26'
- euclean: '117'
- eunatch: '49'
- eusers: '87'
- ewouldblock: '11'
- exdev: '18'
- exfull: '54'
-filename_max: '4096'
-fopen_max: '16'
-has__builtin_va_list: true
-host_name_max: '64'
-int_fast16_t: long
-int_fast32_t: long
-int_fast64_t: long
-int_fast8_t: signed char
-intptr_t: long
-l_tmpnam: '20'
-little_endian: true
-machdep_name: anonymous_machdep
-mb_cur_max: ((size_t)16)
-nsig: (64 + 1)
-path_max: '4096'
-posix_version: 200809L
-ptrdiff_t: long
-rand_max: '2147483647'
-sig_atomic_t: int
-size_t: unsigned long
-sizeof_double: 8
-sizeof_float: 4
-sizeof_fun: 1
-sizeof_int: 4
-sizeof_long: 8
-sizeof_longdouble: 16
-sizeof_longlong: 8
-sizeof_ptr: 8
-sizeof_short: 2
-sizeof_void: 1
-ssize_t: long
-time_t: long
-tmp_max: '238328'
-tty_name_max: '32'
-uint_fast16_t: unsigned long
-uint_fast32_t: unsigned long
-uint_fast64_t: unsigned long
-uint_fast8_t: unsigned char
-uintptr_t: unsigned long
-wchar_t: int
-weof: (0xffffffffu)
-wint_t: int
-wordsize: '64'
diff --git a/tests/fc_script/oracle/estimate_difficulty.err b/tests/fc_script/oracle/estimate_difficulty.err
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/tests/fc_script/oracle/estimate_difficulty.res b/tests/fc_script/oracle/estimate_difficulty.res
deleted file mode 100644
index 30f1b80034aa927ce043a821e1aba9c17be0a536..0000000000000000000000000000000000000000
--- a/tests/fc_script/oracle/estimate_difficulty.res
+++ /dev/null
@@ -1,10 +0,0 @@
-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
-Header-related warnings: 1
diff --git a/tests/fc_script/oracle/find_fun1.res b/tests/fc_script/oracle/find_fun1.res
deleted file mode 100644
index 71eea9bdef1d36da92d821b392155e03e811c21e..0000000000000000000000000000000000000000
--- a/tests/fc_script/oracle/find_fun1.res
+++ /dev/null
@@ -1,6 +0,0 @@
-Looking for 'main2' inside 16 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):
- build-callgraph.i
- main2.c
diff --git a/tests/fc_script/oracle/find_fun2.res b/tests/fc_script/oracle/find_fun2.res
deleted file mode 100644
index 5c9b9b69b9d58907335997f8db1b440930ca63ef..0000000000000000000000000000000000000000
--- a/tests/fc_script/oracle/find_fun2.res
+++ /dev/null
@@ -1,6 +0,0 @@
-Looking for 'main3' inside 16 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):
- build-callgraph.i
- for-find-fun.c
diff --git a/tests/fc_script/oracle/find_fun3.res b/tests/fc_script/oracle/find_fun3.res
deleted file mode 100644
index 67c26fc2681fd115eaca995ff472d4419c48248a..0000000000000000000000000000000000000000
--- a/tests/fc_script/oracle/find_fun3.res
+++ /dev/null
@@ -1,2 +0,0 @@
-Looking for 'false_positive' inside 16 file(s)...
-No declaration/definition found for function 'false_positive'
diff --git a/tests/fc_script/oracle/heuristic_list_functions.res b/tests/fc_script/oracle/heuristic_list_functions.res
deleted file mode 100644
index e6e9c83fdb59cc02b45869c5e9bbbe1c015c15c1..0000000000000000000000000000000000000000
--- a/tests/fc_script/oracle/heuristic_list_functions.res
+++ /dev/null
@@ -1,52 +0,0 @@
-for-find-fun.c:6:7: main2 (declaration)
-for-find-fun.c:13:17: main3 (definition)
-for-find-fun2.c:5:7: main3 (declaration)
-for-find-fun2.c:10:12: f (definition)
-for-find-fun2.c:14:17: g (definition)
-for-find-fun2.c:19:21: h (definition)
-for-find-fun2.c:28:31: static_fun (definition)
-for-list-functions.c:8:15: static_fun (definition)
-for-list-functions.c:17:22: k (definition)
-main.c:17:19: main (definition)
-main2.c:6:8: fake_main (definition)
-main2.c:10:12: domain (definition)
-main2.c:14:16: main2 (definition)
-main3.c:6:9: main (definition)
-make-wrapper.c:10:10: defined (declaration)
-make-wrapper.c:12:12: specified (declaration)
-make-wrapper.c:14:14: external (declaration)
-make-wrapper.c:16:18: large_name_to_force_line_break_in_stack_msg (definition)
-make-wrapper.c:20:22: rec (definition)
-make-wrapper.c:24:30: main (definition)
-make-wrapper2.c:5:7: defined (definition)
-make-wrapper2.c:13:13: specified (declaration)
-make-wrapper2.c:16:16: external (declaration)
-make-wrapper3.c:7:9: external (definition)
-build-callgraph.i:7:9: main (definition)
-build-callgraph.i:16:16: fn2 (declaration)
-build-callgraph.i:18:23: fn1 (definition)
-build-callgraph.i:26:32: main1 (definition)
-build-callgraph.i:34:36: main2 (definition)
-build-callgraph.i:46:49: main3 (definition)
-build-callgraph.i:52:63: main4 (definition)
-build-callgraph.i:64:69: main (definition)
-recursions.i:8:10: g (definition)
-recursions.i:12:15: f (definition)
-recursions.i:17:20: h (definition)
-recursions.i:22:24: i (definition)
-recursions.i:26:28: j (definition)
-recursions.i:30:30: l (declaration)
-recursions.i:31:31: m (declaration)
-recursions.i:33:35: k (definition)
-recursions.i:37:39: l (definition)
-recursions.i:41:43: m (definition)
-recursions.i:45:46: norec (definition)
-recursions.i:48:50: direct_rec (definition)
-recursions.i:52:52: indirect_rec1 (declaration)
-recursions.i:54:56: indirect_rec2 (definition)
-recursions.i:58:60: indirect_rec1 (definition)
-recursions.i:62:62: decl_only (declaration)
-recursions.i:64:64: one_liner_function (definition)
-recursions.i:66:66: multiple_indirect1 (declaration)
-recursions.i:68:71: multiple_indirect2 (definition)
-recursions.i:73:76: multiple_indirect1 (definition)
diff --git a/tests/fc_script/oracle/list_files.res b/tests/fc_script/oracle/list_files.res
deleted file mode 100644
index f6c507d3db5f90b302f072eeb507d76a7d4dc7d3..0000000000000000000000000000000000000000
--- a/tests/fc_script/oracle/list_files.res
+++ /dev/null
@@ -1,10 +0,0 @@
-# Paths as seen by a makefile inside subdirectory '.frama-c':
-SRCS=\
-../main.c \
-../main2.c \
-../main3.c \
-
-
-# Possible definition of main function in the following file(s), as seen from '.frama-c':
-../main.c
-../main3.c
diff --git a/tests/fc_script/oracle/list_functions.res b/tests/fc_script/oracle/list_functions.res
deleted file mode 100644
index 3bc383718c7abdcc03f49c70ac22f3af2c565dd6..0000000000000000000000000000000000000000
--- a/tests/fc_script/oracle/list_functions.res
+++ /dev/null
@@ -1,7 +0,0 @@
-[kernel:typing:implicit-function-declaration] for-find-fun2.c:16: Warning:
- Calling undeclared function false_positive. Old style K&R code?
-f: defined at for-find-fun2.c:10 (1 statement);
-g: defined at for-find-fun2.c:14 (3 statements);
-h: defined at for-find-fun2.c:19 (2 statements);
-k: defined at for-list-functions.c:17 (8 statements);
-static_fun: defined at for-find-fun2.c:28 (1 statement), for-list-functions.c:8 (7 statements);
diff --git a/tests/fc_script/oracle/list_functions2.json b/tests/fc_script/oracle/list_functions2.json
deleted file mode 100644
index feaa24ad887a069b2281c60399e2c713d5c227f5..0000000000000000000000000000000000000000
--- a/tests/fc_script/oracle/list_functions2.json
+++ /dev/null
@@ -1,14 +0,0 @@
-[ { "extf": { "declarations": [ "for-list-functions2.h:1" ] } },
- { "f": { "definitions": [ { "location": "for-find-fun2.c:10",
- "statements": 1 } ] } },
- { "false_positive": { "declarations": [ "for-find-fun2.c:25" ] } },
- { "g": { "definitions": [ { "location": "for-find-fun2.c:14",
- "statements": 3 } ] } },
- { "h": { "definitions": [ { "location": "for-find-fun2.c:19",
- "statements": 2 } ] } },
- { "k": { "definitions": [ { "location": "for-list-functions.c:17",
- "statements": 8 } ] } },
- { "static_fun": { "definitions": [ { "location": "for-find-fun2.c:28",
- "statements": 1 },
- { "location": "for-list-functions.c:8",
- "statements": 7 } ] } } ]
diff --git a/tests/fc_script/oracle/list_functions2.res b/tests/fc_script/oracle/list_functions2.res
deleted file mode 100644
index 2ef35a144fd1397311ad7f9b4c0498f69a6f23bb..0000000000000000000000000000000000000000
--- a/tests/fc_script/oracle/list_functions2.res
+++ /dev/null
@@ -1,3 +0,0 @@
-[kernel:typing:implicit-function-declaration] for-find-fun2.c:16: Warning:
- Calling undeclared function false_positive. Old style K&R code?
-[list-functions] List written to: list_functions2.json
diff --git a/tests/fc_script/oracle/make-wrapper.res b/tests/fc_script/oracle/make-wrapper.res
deleted file mode 100644
index 4d7db660ccc23d7fdb72db0fd967b104b62da771..0000000000000000000000000000000000000000
--- a/tests/fc_script/oracle/make-wrapper.res
+++ /dev/null
@@ -1,17 +0,0 @@
-***** make-wrapper recommendations *****
-
-*** recommendation #1 ***
-
-1. Found recursive call at:
- stack: large_name_to_force_line_break_in_stack_msg :: make-wrapper.c:17 <-
- large_name_to_force_line_break_in_stack_msg :: make-wrapper.c:21 <-
- rec :: make-wrapper.c:26 <-
- main
-
-Consider patching, stubbing or adding an ACSL specification to the recursive call, then re-run the analysis.
-
-*** recommendation #2 ***
-2. Found function with missing specification: large_name_to_force_line_break_in_stack_msg
- Looking for files defining it...
-Add the following file to the list of sources to be parsed:
- make-wrapper.c
diff --git a/tests/fc_script/oracle/make_machdep.err.log b/tests/fc_script/oracle/make_machdep.err.log
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/tests/fc_script/oracle/recursions.res b/tests/fc_script/oracle/recursions.res
deleted file mode 100644
index b6b28585f5646dd057c04df9f862cf7fc378aeee..0000000000000000000000000000000000000000
--- a/tests/fc_script/oracle/recursions.res
+++ /dev/null
@@ -1,18 +0,0 @@
-recursive cycle detected:
- recursions.i:49: direct_rec -> direct_rec
-recursive cycle detected:
- recursions.i:13: f -> f
-recursive cycle detected:
- recursions.i:18: h -> h
-recursive cycle detected:
- recursions.i:59: indirect_rec1 -> indirect_rec2
- recursions.i:55: indirect_rec2 -> indirect_rec1
-recursive cycle detected:
- recursions.i:34: k -> l
- recursions.i:38: l -> m
- recursions.i:42: m -> k
-recursive cycle detected:
- recursions.i:74: multiple_indirect1 -> multiple_indirect2
- recursions.i:75: multiple_indirect1 -> multiple_indirect2
- recursions.i:69: multiple_indirect2 -> multiple_indirect1
- recursions.i:70: multiple_indirect2 -> multiple_indirect1
diff --git a/tests/fc_script/test_config b/tests/fc_script/test_config
deleted file mode 100644
index 11c2e8173b5b072f0e234344a289457747b7cb36..0000000000000000000000000000000000000000
--- a/tests/fc_script/test_config
+++ /dev/null
@@ -1,7 +0,0 @@
-/* run.config*
-COMMENT: Explicits the dependencies of {bin:frama-c-script} execution:
- PLUGIN: variadic,instantiate
-COMMENT: The library frama-c.analysis_scripts is part of the package frama-c
-COMMENT: and this dependency is implicit as the one to the needed python files.
-ENABLED_IF: %{read:../../../python-3.7-available}
-*/
diff --git a/tests/fc_script/test_machdep.i b/tests/fc_script/test_machdep.i
deleted file mode 100644
index 923485dde8e59c0631db3e506d95a6c23cf4699b..0000000000000000000000000000000000000000
--- a/tests/fc_script/test_machdep.i
+++ /dev/null
@@ -1,12 +0,0 @@
-/* run.config
- NOFRAMAC: Just test the generation of a custom machdep with the installed script.
- COMMENT: No C code gets analyzed there. File is empty on purpose
- COMMENT: be sure to keep the first EXECNOW: it ensures
- COMMENT: that dune will copy the file regardless of the environment
- COMMENT: so that other tests whose oracles depend on the number of file in
- COMMENT: the directory will be stable.
- EXECNOW: LOG empty.res touch empty.res
- ENABLED_IF: (and %{bin-available:clang} %{bin-available:yq})
- FILTER: sed -e '/^version:/d'
- EXECNOW: LOG custom_machdep.yaml LOG make_machdep.err.log PTESTS_TESTING=1 %{bin:frama-c-script} make-machdep --compiler clang --cpp-arch-flags='--target=x86_64' | yq -Y 'del(.version)|del(.custom_defs)' > custom_machdep.yaml 2> make_machdep.err.log
-*/
diff --git a/tests/ptests_config b/tests/ptests_config
index 1df830115c750baa5eb44fd157a1e90054422381..cac61a035729f47fde2b0f896f1859e497b5dcad 100644
--- a/tests/ptests_config
+++ b/tests/ptests_config
@@ -4,7 +4,7 @@
### Tests of kernel
-DEFAULT_SUITES= cil compliance dynamic fc_script jcdb libc misc
+DEFAULT_SUITES= cil compliance dynamic jcdb libc misc
DEFAULT_SUITES= pretty_printing saveload spec syntax test
### Tests of small plugins