diff --git a/src/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml index e3c92e75a42f4a775c52c41233fe388559f4dfe2..f57033cb1366c7c76c3e10849634fd9e213c2261 100644 --- a/src/plugins/server/kernel_main.ml +++ b/src/plugins/server/kernel_main.ml @@ -90,10 +90,15 @@ struct let to_json p = let path = Filepath.(Normalized.to_pretty_string p.pos_path) in + let file = + if Server_parameters.has_relative_filepath () + then path + else (p.Filepath.pos_path :> string) + in `Assoc [ "dir" , `String (Filename.dirname path) ; "base" , `String (Filename.basename path) ; - "file" , `String (p.Filepath.pos_path :> string) ; + "file" , `String file ; "line" , `Int p.Filepath.pos_lnum ; ] diff --git a/src/plugins/server/server_parameters.ml b/src/plugins/server/server_parameters.ml index be9b5da15c6ad6f271c9bd6cb764422eee3f0cfa..74a07c43b7f08e171044e3fd0c8c0c1d8a98adff 100644 --- a/src/plugins/server/server_parameters.ml +++ b/src/plugins/server/server_parameters.ml @@ -73,3 +73,10 @@ let wkind = register_warn_category "inconsistent-kind" let wname = register_warn_category "invalid-name" (* -------------------------------------------------------------------------- *) +(* --- Filepath Normalization --- *) +(* -------------------------------------------------------------------------- *) + +let use_relative_filepath = register_category "use-relative-filepath" +let has_relative_filepath () = is_debug_key_enabled use_relative_filepath + +(* -------------------------------------------------------------------------- *) diff --git a/src/plugins/server/server_parameters.mli b/src/plugins/server/server_parameters.mli index af8c6dea9d1aa600df8d3cf09bf5fd74a9a4db6c..ba41ba164c75e313f8a74a78dd710e1e5273d704 100644 --- a/src/plugins/server/server_parameters.mli +++ b/src/plugins/server/server_parameters.mli @@ -32,4 +32,6 @@ val wpage : warn_category (** Inconsistent page warning *) val wkind : warn_category (** Inconsistent category warning *) val wname : warn_category (** Invalid name warning *) +val has_relative_filepath: unit -> bool + (**************************************************************************) diff --git a/src/plugins/server/tests/batch/oracle/ast_services.out.json b/src/plugins/server/tests/batch/oracle/ast_services.out.json index 5ecfe153b226bca9952c46562f2b0408a4827e1f..a6223032cf20850343a7d0270679a14b24daee0b 100644 --- a/src/plugins/server/tests/batch/oracle/ast_services.out.json +++ b/src/plugins/server/tests/batch/oracle/ast_services.out.json @@ -11,8 +11,7 @@ "sloc": { "dir": "tests/batch", "base": "ast_services.i", - "file": - "/home/michele/work/frama-c/src/plugins/server/tests/batch/ast_services.i", + "file": "tests/batch/ast_services.i", "line": 2 } }, @@ -24,8 +23,7 @@ "sloc": { "dir": "tests/batch", "base": "ast_services.i", - "file": - "/home/michele/work/frama-c/src/plugins/server/tests/batch/ast_services.i", + "file": "tests/batch/ast_services.i", "line": 1 } } diff --git a/src/plugins/server/tests/batch/test_config b/src/plugins/server/tests/batch/test_config index 15a16cd4f95d4ced405bb04b6a13382efcd47e7f..4addf96dff82842ab79ae170fda242244765a7c0 100644 --- a/src/plugins/server/tests/batch/test_config +++ b/src/plugins/server/tests/batch/test_config @@ -1,2 +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@ +OPT: -no-autoload-plugins -load-module server -check -server-batch @PTEST_DIR@/@PTEST_NAME@.json -server-batch-output-dir @PTEST_RESULT@ -server-msg-key use-relative-filepath