diff --git a/src/plugins/server/Makefile.in b/src/plugins/server/Makefile.in
index f70395724dae585cc902a00f8ca0dcc190d9ace0..4035bc252a9bffce81e5de5b686fba20e51908cb 100644
--- a/src/plugins/server/Makefile.in
+++ b/src/plugins/server/Makefile.in
@@ -29,17 +29,13 @@ ifndef FRAMAC_LIBDIR
FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
endif
-include $(FRAMAC_SHARE)/Makefile.config
-# --------------------------------------------------------------------------
-# --- Plugin Setting
-# --------------------------------------------------------------------------
+###################
+# Plug-in Setting #
+###################
+PLUGIN_DIR ?=.
PLUGIN_ENABLE:=@ENABLE_SERVER@
PLUGIN_NAME:=Server
-PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
-PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
-
-PLUGIN_REQUIRES:= yojson
PLUGIN_CMO:= \
server_parameters \
jbuffer \
@@ -48,30 +44,34 @@ PLUGIN_CMO:= \
kernel_main \
kernel_project \
kernel_ast
+PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
+PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
+PLUGIN_TESTS_DIRS := batch
+
+PLUGIN_REQUIRES:= yojson
PLUGIN_UNDOC:= server_batch.ml server_zmq.ml
PLUGIN_GENERATED:= $(PLUGIN_DIR)/Server.mli
-PLUGIN_TESTS :=
-# --------------------------------------------------------------------------
-# --- ZeroMQ Support
-# --------------------------------------------------------------------------
+##################
+# ZeroMQ Support #
+##################
ifeq (@SERVER_ZMQ@,yes)
PLUGIN_REQUIRES+= zmq
PLUGIN_CMO+= server_zmq
endif
-# --------------------------------------------------------------------------
-# --- Frama-C Dynamic Plug-in
-# --------------------------------------------------------------------------
+################
+# Generic part #
+################
include $(FRAMAC_SHARE)/Makefile.dynamic
-# --------------------------------------------------------------------------
-# --- Server API
-# --------------------------------------------------------------------------
+##############
+# Server API #
+##############
SERVER_API= \
doc.mli syntax.mli data.mli request.mli
@@ -100,9 +100,9 @@ $(Server_DIR)/Server.mli: $(Server_DIR)/Makefile $(SERVER_MLI)
$(CHMOD_RO) $@.tmp
$(MV) $@.tmp $@
-# --------------------------------------------------------------------------
-# --- Configure
-# --------------------------------------------------------------------------
+#####################################
+# Regenerating the Makefile on need #
+#####################################
ifeq ("$(FRAMAC_INTERNAL)","yes")
CONFIG_STATUS_DIR=$(FRAMAC_SRC)
@@ -113,5 +113,3 @@ endif
$(Server_DIR)/Makefile: $(Server_DIR)/Makefile.in \
$(CONFIG_STATUS_DIR)/config.status
cd $(CONFIG_STATUS_DIR) && ./config.status --file $@
-
-# --------------------------------------------------------------------------
diff --git a/src/plugins/server/server_batch.ml b/src/plugins/server/server_batch.ml
index 0aa3c03b310a2c1104baf91a712a17bd17a9f01b..87a3fd9c4907562237c4d23e495f91397a59df10 100644
--- a/src/plugins/server/server_batch.ml
+++ b/src/plugins/server/server_batch.ml
@@ -41,8 +41,19 @@ module Batch = Senv.String_list
associated results in <file.out.json>."
end)
+let () = Parameter_customize.set_group batch_group
+module BatchOutputDir = Senv.Empty_string
+ (struct
+ let option_name = "-server-batch-output-dir"
+ let arg_name = "path"
+ let help =
+ "Outputs the results of -server-batch in <path> instead of the input \
+ directory."
+ end)
+
let _ = Doc.page `Protocol ~title:"Batch Protocol" ~filename:"server_batch.md"
+
(* -------------------------------------------------------------------------- *)
(* --- Execute JSON --- *)
(* -------------------------------------------------------------------------- *)
@@ -64,9 +75,8 @@ let execute_command js =
try
Senv.feedback "[%a] %s" Main.pp_kind kind request ;
`Assoc [ "id" , id ; "data" , handler data ]
- with Ju.Type_error(msg,js) ->
- Senv.error "[%s] incorrect encoding:@\n%s@\n@[<hov 2>At: %a@]@."
- request msg pretty js ;
+ with Data.InputError(msg) ->
+ Senv.error "[%s] %s@." request msg ;
`Assoc [ "id" , id ; "error" , `String msg ; "at" , js ]
let rec execute_batch js =
@@ -90,9 +100,15 @@ let execute () =
begin fun file ->
Senv.feedback "Script %S" file ;
let response = execute_batch (Js.from_file file) in
- let output = Filename.remove_extension file ^ ".out.js" in
+ let output = Filename.remove_extension file ^ ".out.json" in
+ let output = match BatchOutputDir.get () with
+ | "" -> output
+ | dir -> Filename.(dir ^ dir_sep ^ basename output)
+ in
Senv.feedback "Output %S" output ;
- Js.to_file output response ;
+ let out = open_out output in
+ Js.pretty_to_channel out response ;
+ close_out out
end
(Batch.get()) ;
end
diff --git a/src/plugins/server/tests/.gitignore b/src/plugins/server/tests/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..e2f5dd2eb20cb10838ae60e263317b57fdec63e7
--- /dev/null
+++ b/src/plugins/server/tests/.gitignore
@@ -0,0 +1 @@
+result
\ No newline at end of file
diff --git a/src/plugins/server/tests/batch/ast_services.i b/src/plugins/server/tests/batch/ast_services.i
new file mode 100644
index 0000000000000000000000000000000000000000..b875167edd1a3b6d5904bb4db378c8be91b18310
--- /dev/null
+++ b/src/plugins/server/tests/batch/ast_services.i
@@ -0,0 +1,2 @@
+void main() {}
+void f() {}
\ No newline at end of file
diff --git a/src/plugins/server/tests/batch/ast_services.json b/src/plugins/server/tests/batch/ast_services.json
new file mode 100644
index 0000000000000000000000000000000000000000..45254f96445b99992be0bc44a46207c195e72b54
--- /dev/null
+++ b/src/plugins/server/tests/batch/ast_services.json
@@ -0,0 +1,4 @@
+[
+ { id:"getFunctions", request:"kernel.ast.getFunctions", data:null },
+ { id:"printFunction", request:"kernel.ast.printFunction", data:"f" }
+]
\ No newline at end of file
diff --git a/src/plugins/server/tests/batch/kernel_services.i b/src/plugins/server/tests/batch/kernel_services.i
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/server/tests/batch/kernel_services.json b/src/plugins/server/tests/batch/kernel_services.json
new file mode 100644
index 0000000000000000000000000000000000000000..5b58c627bfe01240de30931928d88a35352fbc83
--- /dev/null
+++ b/src/plugins/server/tests/batch/kernel_services.json
@@ -0,0 +1,4 @@
+[
+ { id:"getLogs", request:"kernel.getLogs", data:null },
+ { id:"setLogs", request:"kernel.setLogs", data:false }
+]
\ No newline at end of file
diff --git a/src/plugins/server/tests/batch/oracle/ast_services.out.json b/src/plugins/server/tests/batch/oracle/ast_services.out.json
new file mode 100644
index 0000000000000000000000000000000000000000..40a40546e0dd93809a46d584a1df5efa783faf27
--- /dev/null
+++ b/src/plugins/server/tests/batch/oracle/ast_services.out.json
@@ -0,0 +1,14 @@
+[
+ { "id": "getFunctions", "data": [ "f", "main" ] },
+ {
+ "id": "printFunction",
+ "data": [
+ "",
+ [ "#v19", "void f(void)" ],
+ "\n{\n ",
+ [ "#s7", [ "#k7", "return;" ] ],
+ "\n}\n",
+ "\n"
+ ]
+ }
+]
\ No newline at end of file
diff --git a/src/plugins/server/tests/batch/oracle/ast_services.res.oracle b/src/plugins/server/tests/batch/oracle/ast_services.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f91a4f9d11d9733287e6673255e3dc07ccf12def
--- /dev/null
+++ b/src/plugins/server/tests/batch/oracle/ast_services.res.oracle
@@ -0,0 +1,5 @@
+[kernel] Parsing tests/batch/ast_services.i (no preprocessing)
+[server] Script "tests/batch/ast_services.json"
+[server] [GET] kernel.ast.getFunctions
+[server] [GET] kernel.ast.printFunction
+[server] Output "tests/batch/result/ast_services.out.json"
diff --git a/src/plugins/server/tests/batch/oracle/kernel_services.out.json b/src/plugins/server/tests/batch/oracle/kernel_services.out.json
new file mode 100644
index 0000000000000000000000000000000000000000..80065331f0735613e4a74e0a75df36f60d10ac4f
--- /dev/null
+++ b/src/plugins/server/tests/batch/oracle/kernel_services.out.json
@@ -0,0 +1 @@
+[ { "id": "getLogs", "data": [] }, { "id": "setLogs", "data": null } ]
\ No newline at end of file
diff --git a/src/plugins/server/tests/batch/oracle/kernel_services.res.oracle b/src/plugins/server/tests/batch/oracle/kernel_services.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7e1c091eeec6f5d3fdd51a5d05c677f0e1fee812
--- /dev/null
+++ b/src/plugins/server/tests/batch/oracle/kernel_services.res.oracle
@@ -0,0 +1,5 @@
+[kernel] Parsing tests/batch/kernel_services.i (no preprocessing)
+[server] Script "tests/batch/kernel_services.json"
+[server] [GET] kernel.getLogs
+[server] [SET] kernel.setLogs
+[server] Output "tests/batch/result/kernel_services.out.json"
diff --git a/src/plugins/server/tests/batch/oracle/wrong.out.json b/src/plugins/server/tests/batch/oracle/wrong.out.json
new file mode 100644
index 0000000000000000000000000000000000000000..4bf1761a32d70d5658b681897a5b5278f43511f8
--- /dev/null
+++ b/src/plugins/server/tests/batch/oracle/wrong.out.json
@@ -0,0 +1,14 @@
+[
+ { "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"
+ }
+ }
+]
\ No newline at end of file
diff --git a/src/plugins/server/tests/batch/oracle/wrong.res.oracle b/src/plugins/server/tests/batch/oracle/wrong.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..76ac96361f0316a6703142ce491f2500e89790ee
--- /dev/null
+++ b/src/plugins/server/tests/batch/oracle/wrong.res.oracle
@@ -0,0 +1,9 @@
+[kernel] Parsing tests/batch/wrong.i (no preprocessing)
+[server] Script "tests/batch/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 "tests/batch/result/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/test_config b/src/plugins/server/tests/batch/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..15a16cd4f95d4ced405bb04b6a13382efcd47e7f
--- /dev/null
+++ b/src/plugins/server/tests/batch/test_config
@@ -0,0 +1,2 @@
+LOG: @PTEST_NAME@.out.json
+OPT: -no-autoload-plugins -load-module server -check -server-batch @PTEST_DIR@/@PTEST_NAME@.json -server-batch-output-dir @PTEST_RESULT@
diff --git a/src/plugins/server/tests/batch/wrong.i b/src/plugins/server/tests/batch/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.json
new file mode 100644
index 0000000000000000000000000000000000000000..0178e8af2950cbc6b6a49d98367265e2bf993989
--- /dev/null
+++ b/src/plugins/server/tests/batch/wrong.json
@@ -0,0 +1,4 @@
+[
+ { id:"unknown request", request:"kernel.unknown", data:null, comment:"the request doesn't exist" },
+ { id:"wrong data", request:"kernel.ast.printFunction", data:{f1:1, f2:{x:1, y:2}, f3:null}, comment:"ident is expected, object is given" }
+]
\ No newline at end of file