diff --git a/nix/kernel-tests.nix b/nix/kernel-tests.nix
index 5fa1c0096d2945ddd0d07d183dd63271c7d9f448..92fe1d96eb41c2bc836f372ec56fea3cf0d4fc20 100644
--- a/nix/kernel-tests.nix
+++ b/nix/kernel-tests.nix
@@ -16,7 +16,8 @@ mk_tests {
@tests/syntax/ptests \
@tests/test/ptests \
@src/kernel_internals/parsing/tests/ptests
- dune runtest \
+ dune runtest -j1 --display short \
+ src/plugins/server/tests/batch \
tests/fc_script
'';
}
diff --git a/src/plugins/server/tests/batch/ast_services.i b/src/plugins/server/tests/batch/ast_services.t/ast_services.i
similarity index 59%
rename from src/plugins/server/tests/batch/ast_services.i
rename to src/plugins/server/tests/batch/ast_services.t/ast_services.i
index 4c1e7b1b838700580f438bdcd4ca35bc4db693d9..975369e8966a949daaa79f906923989730a7e8ce 100644
--- a/src/plugins/server/tests/batch/ast_services.i
+++ b/src/plugins/server/tests/batch/ast_services.t/ast_services.i
@@ -1,8 +1,2 @@
-/* run.config*
- EXIT: 1
- STDOPT:
-*/
-
-
int f(int x) { return x++; }
int g(int y) { return y++; }
diff --git a/src/plugins/server/tests/batch/ast_services.json b/src/plugins/server/tests/batch/ast_services.t/ast_services.json
similarity index 100%
rename from src/plugins/server/tests/batch/ast_services.json
rename to src/plugins/server/tests/batch/ast_services.t/ast_services.json
diff --git a/src/plugins/server/tests/batch/ast_services.t/run.t b/src/plugins/server/tests/batch/ast_services.t/run.t
new file mode 100644
index 0000000000000000000000000000000000000000..94344fd5ed668105a8bc5a25dc4409a7bba14365
--- /dev/null
+++ b/src/plugins/server/tests/batch/ast_services.t/run.t
@@ -0,0 +1,129 @@
+ $ frama-c -no-autoload-plugins -load-plugin server ast_services.i -server-batch ast_services.json -server-msg-key use-relative-filepath
+ [kernel] Parsing ast_services.i (no preprocessing)
+ [server] Script "ast_services.json"
+ [server] [GET] kernel.ast.fetchFunctions
+ [server] [GET] kernel.ast.fetchFunctions
+ [server] [GET] kernel.ast.printFunction
+ [server] [GET] kernel.ast.printFunction
+ [server] [GET] kernel.ast.printFunction
+ [server] User Error: [kernel.ast.printFunction] Undefined function 'h'
+ [server] Output "ast_services.out.json"
+ [server] User Error: Deferred error message was emitted during execution. See above messages for more information.
+ [kernel] Plug-in server aborted: invalid user input.
+ [1]
+ $ cat ast_services.out.json
+ [
+ {
+ "id": "GET-1",
+ "data": {
+ "updated": [
+ {
+ "key": "kf#24",
+ "name": "g",
+ "signature": "int g(int y);",
+ "defined": true,
+ "sloc": {
+ "dir": ".",
+ "base": "ast_services.i",
+ "file": "ast_services.i",
+ "line": 2
+ }
+ },
+ {
+ "key": "kf#20",
+ "name": "f",
+ "signature": "int f(int x);",
+ "defined": true,
+ "sloc": {
+ "dir": ".",
+ "base": "ast_services.i",
+ "file": "ast_services.i",
+ "line": 1
+ }
+ }
+ ],
+ "removed": [],
+ "reload": true,
+ "pending": 0
+ }
+ },
+ {
+ "id": "GET-2",
+ "data": { "updated": [], "removed": [], "reload": false, "pending": 0 }
+ },
+ {
+ "id": "PRINT-F",
+ "data": [
+ "",
+ [
+ "#v20",
+ [ "#y1", "int" ],
+ " f(",
+ [ "#v22", [ "#y1", "int" ], " x" ],
+ ")"
+ ],
+ "\n{\n ",
+ [ "#v23", [ "#y1", "int" ], " tmp" ],
+ ";\n ",
+ [
+ "#s1",
+ [
+ "#k1",
+ "{ /* sequence */\n ",
+ [ "#s2", [ "#k2", [ "#l2", "tmp" ], " = ", [ "#l3", "x" ], ";" ] ],
+ "\n ",
+ [ "#s3", [ "#k3", [ "#l4", "x" ], " ++;" ] ],
+ "\n ",
+ [ "#s4", [ "#k4", ";" ] ],
+ "\n }"
+ ]
+ ],
+ "\n ",
+ [ "#s5", [ "#k5", "return ", [ "#l5", "tmp" ], ";" ] ],
+ "\n}\n",
+ "\n"
+ ]
+ },
+ {
+ "id": "PRINT-G",
+ "data": [
+ "",
+ [
+ "#v24",
+ [ "#y1", "int" ],
+ " g(",
+ [ "#v26", [ "#y1", "int" ], " y" ],
+ ")"
+ ],
+ "\n{\n ",
+ [ "#v27", [ "#y1", "int" ], " tmp" ],
+ ";\n ",
+ [
+ "#s7",
+ [
+ "#k7",
+ "{ /* sequence */\n ",
+ [ "#s8", [ "#k8", [ "#l6", "tmp" ], " = ", [ "#l7", "y" ], ";" ] ],
+ "\n ",
+ [ "#s9", [ "#k9", [ "#l8", "y" ], " ++;" ] ],
+ "\n ",
+ [ "#s10", [ "#k10", ";" ] ],
+ "\n }"
+ ]
+ ],
+ "\n ",
+ [ "#s11", [ "#k11", "return ", [ "#l9", "tmp" ], ";" ] ],
+ "\n}\n",
+ "\n"
+ ]
+ },
+ {
+ "id": "PRINT-H",
+ "error": "Undefined function 'h'",
+ "at": {
+ "id": "PRINT-H",
+ "request": "kernel.ast.printFunction",
+ "data": "h"
+ }
+ }
+ ]
diff --git a/src/plugins/server/tests/batch/oracle/ast_services.out.json b/src/plugins/server/tests/batch/oracle/ast_services.out.json
deleted file mode 100644
index fb290fcefc3d106a1749c161102334612aed52c4..0000000000000000000000000000000000000000
--- a/src/plugins/server/tests/batch/oracle/ast_services.out.json
+++ /dev/null
@@ -1,115 +0,0 @@
-[
- {
- "id": "GET-1",
- "data": {
- "updated": [
- {
- "key": "kf#24",
- "name": "g",
- "signature": "int g(int y);",
- "defined": true,
- "sloc": {
- "dir": ".",
- "base": "ast_services.i",
- "file": "ast_services.i",
- "line": 8
- }
- },
- {
- "key": "kf#20",
- "name": "f",
- "signature": "int f(int x);",
- "defined": true,
- "sloc": {
- "dir": ".",
- "base": "ast_services.i",
- "file": "ast_services.i",
- "line": 7
- }
- }
- ],
- "removed": [],
- "reload": true,
- "pending": 0
- }
- },
- {
- "id": "GET-2",
- "data": { "updated": [], "removed": [], "reload": false, "pending": 0 }
- },
- {
- "id": "PRINT-F",
- "data": [
- "",
- [
- "#v20",
- [ "#y1", "int" ],
- " f(",
- [ "#v22", [ "#y1", "int" ], " x" ],
- ")"
- ],
- "\n{\n ",
- [ "#v23", [ "#y1", "int" ], " tmp" ],
- ";\n ",
- [
- "#s1",
- [
- "#k1",
- "{ /* sequence */\n ",
- [ "#s2", [ "#k2", [ "#l2", "tmp" ], " = ", [ "#l3", "x" ], ";" ] ],
- "\n ",
- [ "#s3", [ "#k3", [ "#l4", "x" ], " ++;" ] ],
- "\n ",
- [ "#s4", [ "#k4", ";" ] ],
- "\n }"
- ]
- ],
- "\n ",
- [ "#s5", [ "#k5", "return ", [ "#l5", "tmp" ], ";" ] ],
- "\n}\n",
- "\n"
- ]
- },
- {
- "id": "PRINT-G",
- "data": [
- "",
- [
- "#v24",
- [ "#y1", "int" ],
- " g(",
- [ "#v26", [ "#y1", "int" ], " y" ],
- ")"
- ],
- "\n{\n ",
- [ "#v27", [ "#y1", "int" ], " tmp" ],
- ";\n ",
- [
- "#s7",
- [
- "#k7",
- "{ /* sequence */\n ",
- [ "#s8", [ "#k8", [ "#l6", "tmp" ], " = ", [ "#l7", "y" ], ";" ] ],
- "\n ",
- [ "#s9", [ "#k9", [ "#l8", "y" ], " ++;" ] ],
- "\n ",
- [ "#s10", [ "#k10", ";" ] ],
- "\n }"
- ]
- ],
- "\n ",
- [ "#s11", [ "#k11", "return ", [ "#l9", "tmp" ], ";" ] ],
- "\n}\n",
- "\n"
- ]
- },
- {
- "id": "PRINT-H",
- "error": "Undefined function 'h'",
- "at": {
- "id": "PRINT-H",
- "request": "kernel.ast.printFunction",
- "data": "h"
- }
- }
-]
diff --git a/src/plugins/server/tests/batch/oracle/ast_services.res.oracle b/src/plugins/server/tests/batch/oracle/ast_services.res.oracle
deleted file mode 100644
index d41568131c96a7f1209a1d77364b4c88dc316475..0000000000000000000000000000000000000000
--- a/src/plugins/server/tests/batch/oracle/ast_services.res.oracle
+++ /dev/null
@@ -1,11 +0,0 @@
-[kernel] Parsing ast_services.i (no preprocessing)
-[server] Script "./ast_services.json"
-[server] [GET] kernel.ast.fetchFunctions
-[server] [GET] kernel.ast.fetchFunctions
-[server] [GET] kernel.ast.printFunction
-[server] [GET] kernel.ast.printFunction
-[server] [GET] kernel.ast.printFunction
-[server] User Error: [kernel.ast.printFunction] Undefined function 'h'
-[server] Output "./ast_services.out.json"
-[server] User Error: Deferred error message was emitted during execution. See above messages for more information.
-[kernel] Plug-in server aborted: invalid user input.
diff --git a/src/plugins/server/tests/batch/oracle/wrong.out.json b/src/plugins/server/tests/batch/oracle/wrong.out.json
deleted file mode 100644
index e083e787f78e5c7848fe16123698d5d618f41d70..0000000000000000000000000000000000000000
--- a/src/plugins/server/tests/batch/oracle/wrong.out.json
+++ /dev/null
@@ -1,13 +0,0 @@
-[
- { "id": "unknown request", "error": "request not found" },
- {
- "id": "wrong data",
- "error": "Expected string, got object:\n{ \"f1\": 1, \"f2\": { \"x\": 1, \"y\": 2 }, \"f3\": null }",
- "at": {
- "id": "wrong data",
- "request": "kernel.ast.printFunction",
- "data": { "f1": 1, "f2": { "x": 1, "y": 2 }, "f3": null },
- "comment": "ident is expected, object is given"
- }
- }
-]
diff --git a/src/plugins/server/tests/batch/oracle/wrong.res.oracle b/src/plugins/server/tests/batch/oracle/wrong.res.oracle
deleted file mode 100644
index 2683b91d309978f076361a05034081da2d055292..0000000000000000000000000000000000000000
--- a/src/plugins/server/tests/batch/oracle/wrong.res.oracle
+++ /dev/null
@@ -1,9 +0,0 @@
-[kernel] Parsing wrong.i (no preprocessing)
-[server] Script "./wrong.json"
-[server] User Error: [batch] "unknown request": request "kernel.unknown" not found
-[server] [GET] kernel.ast.printFunction
-[server] User Error: [kernel.ast.printFunction] Expected string, got object:
- { "f1": 1, "f2": { "x": 1, "y": 2 }, "f3": null }
-[server] Output "./wrong.out.json"
-[server] User Error: Deferred error message was emitted during execution. See above messages for more information.
-[kernel] Plug-in server aborted: invalid user input.
diff --git a/src/plugins/server/tests/batch/wrong.i b/src/plugins/server/tests/batch/wrong.i
deleted file mode 100644
index 1a0a6550cd22661cdae17a41fdd59cc8e2709201..0000000000000000000000000000000000000000
--- a/src/plugins/server/tests/batch/wrong.i
+++ /dev/null
@@ -1,4 +0,0 @@
-/* run.config*
- EXIT: 1
- STDOPT:
-*/
diff --git a/src/plugins/server/tests/batch/wrong.t/run.t b/src/plugins/server/tests/batch/wrong.t/run.t
new file mode 100644
index 0000000000000000000000000000000000000000..689703d439a55a2251a21fdb70d89c7279c3e01f
--- /dev/null
+++ b/src/plugins/server/tests/batch/wrong.t/run.t
@@ -0,0 +1,25 @@
+ $ frama-c -no-autoload-plugins -load-plugin server wrong.i -server-batch wrong.json -server-msg-key use-relative-filepath
+ [kernel] Parsing wrong.i (no preprocessing)
+ [server] Script "wrong.json"
+ [server] User Error: [batch] "unknown request": request "kernel.unknown" not found
+ [server] [GET] kernel.ast.printFunction
+ [server] User Error: [kernel.ast.printFunction] Expected string, got object:
+ { "f1": 1, "f2": { "x": 1, "y": 2 }, "f3": null }
+ [server] Output "wrong.out.json"
+ [server] User Error: Deferred error message was emitted during execution. See above messages for more information.
+ [kernel] Plug-in server aborted: invalid user input.
+ [1]
+ $ cat wrong.out.json
+ [
+ { "id": "unknown request", "error": "request not found" },
+ {
+ "id": "wrong data",
+ "error": "Expected string, got object:\n{ \"f1\": 1, \"f2\": { \"x\": 1, \"y\": 2 }, \"f3\": null }",
+ "at": {
+ "id": "wrong data",
+ "request": "kernel.ast.printFunction",
+ "data": { "f1": 1, "f2": { "x": 1, "y": 2 }, "f3": null },
+ "comment": "ident is expected, object is given"
+ }
+ }
+ ]
diff --git a/src/plugins/server/tests/batch/wrong.t/wrong.i b/src/plugins/server/tests/batch/wrong.t/wrong.i
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/server/tests/batch/wrong.json b/src/plugins/server/tests/batch/wrong.t/wrong.json
similarity index 100%
rename from src/plugins/server/tests/batch/wrong.json
rename to src/plugins/server/tests/batch/wrong.t/wrong.json