diff --git a/nix/internal-tests.nix b/nix/internal-tests.nix
index 38e6e924e0b2868a34b0cc9f5ac80d0541c7f969..ebce2ac5341483ccf0b8dddeaae5bde1ce99435a 100644
--- a/nix/internal-tests.nix
+++ b/nix/internal-tests.nix
@@ -54,6 +54,7 @@
, perl
, python3
, python3Packages
+, socat
, swi-prolog
, time
, unixtools
@@ -128,6 +129,7 @@ stdenvNoCC.mkDerivation rec {
python3
python3Packages.jsonschema
python3Packages.pyaml
+ socat
swi-prolog
time
unixtools.getopt
diff --git a/nix/mk_tests.nix b/nix/mk_tests.nix
index 81e3c3f6a6e2b65859b8a075e24cd4ad24ec783d..b24ee61011990023511e357fa04a25bb582cde0a 100644
--- a/nix/mk_tests.nix
+++ b/nix/mk_tests.nix
@@ -34,6 +34,7 @@
, jq
, perl
, python3Packages
+, socat
, stdenvNoCC
, time
, unixtools
@@ -65,6 +66,7 @@ stdenvNoCC.mkDerivation {
perl
python3Packages.jsonschema
python3Packages.pyaml
+ socat
time
unixtools.getopt
which
diff --git a/src/kernel_services/plugin_entry_points/log.ml b/src/kernel_services/plugin_entry_points/log.ml
index 10a4ec0697ffe7c600de4fb8a291f9e07e6d8159..88146911ff78da13a9b13aacbe18f0fa025d3661 100644
--- a/src/kernel_services/plugin_entry_points/log.ml
+++ b/src/kernel_services/plugin_entry_points/log.ml
@@ -20,6 +20,9 @@
(* *)
(**************************************************************************)
+(* Messages longer than N characters are truncated when printed on terminal. *)
+let max_message_length = 10000
+
type kind = Result | Feedback | Debug | Warning | Error | Failure
[@@@ warning "-32"]
@@ -467,6 +470,7 @@ let logtransient channel text =
try
Format.pp_print_newline fmt () ;
Format.pp_print_flush fmt () ;
+ ignore (Rich_text.truncate buffer max_message_length) ;
let p,q = Rich_text.trim buffer in
do_transient channel.terminal (Rich_text.contents buffer) p q ;
close_buffer channel
@@ -497,11 +501,19 @@ let logwithfinal finally channel
Format.pp_close_box fmt () ;
Format.pp_print_newline fmt () ;
Format.pp_print_flush fmt () ;
+ let truncated =
+ if channel.terminal.isatty
+ then Rich_text.truncate buffer max_message_length
+ else false
+ in
let p,q = Rich_text.trim buffer in
let output =
if p <= q then
let source = get_source current source in
let message = Rich_text.range buffer p q in
+ let message =
+ if truncated then "(truncated message) " ^ message else message
+ in
let event = {
evt_kind = kind ;
evt_plugin = channel.plugin ;
diff --git a/src/libraries/utils/rich_text.ml b/src/libraries/utils/rich_text.ml
index 3d08c1cd3f6977288219889a6c0c9e60f1d39411..1e1d2220129f994acf95965d78108d1b8b650a22 100644
--- a/src/libraries/utils/rich_text.ml
+++ b/src/libraries/utils/rich_text.ml
@@ -106,8 +106,6 @@ let pretty ?vbox fmt message =
(* -------------------------------------------------------------------------- *)
let min_buffer = 128 (* initial size of buffer *)
-let max_buffer = 2097152 (* maximal size of buffer *)
-let tgr_buffer = 3145728 (* elasticity (internal overhead) *)
type buffer = {
mutable formatter : Format.formatter ; (* formatter on self (recursive) *)
@@ -136,7 +134,8 @@ let shrink buffer =
if Buffer.length buffer.content > min_buffer then
Buffer.reset buffer.content
-let truncate_text buffer size =
+let truncate buffer size =
+ let truncated = ref false in
if Buffer.length buffer.content > size then
begin
let p = trim_begin buffer in
@@ -147,23 +146,21 @@ let truncate_text buffer size =
else if n <= size then
Buffer.blit buffer.content p (Buffer.to_bytes buffer.content) 0 n
else
- begin
- let n_left = size / 2 - 3 in
- let n_right = size - n_left - 5 in
- if p > 0 then
- Buffer.blit buffer.content p (Buffer.to_bytes buffer.content) 0 n_left;
- let buf_right = Buffer.sub buffer.content (q-n_right+1) n_right in
- Buffer.truncate buffer.content n_left;
- Buffer.add_string buffer.content "[...]";
- Buffer.add_string buffer.content buf_right;
- end
- end
+ let n_left = size / 2 - 3 in
+ let n_right = size - n_left - 5 in
+ if p > 0 then
+ Buffer.blit buffer.content p (Buffer.to_bytes buffer.content) 0 n_left;
+ let buf_right = Buffer.sub buffer.content (q-n_right+1) n_right in
+ Buffer.truncate buffer.content n_left;
+ Buffer.add_string buffer.content "[...]";
+ Buffer.add_string buffer.content buf_right;
+ truncated := true;
+ end;
+ !truncated
(* All text added shall go through this function *)
let append buffer s k n =
- Buffer.add_substring buffer.content s k n ;
- if Buffer.length buffer.content > tgr_buffer then
- truncate_text buffer max_buffer
+ Buffer.add_substring buffer.content s k n
let push_tag buffer _tag =
let p = Buffer.length buffer.content in
@@ -219,13 +216,12 @@ let create ?indent ?margin () =
buffer
let trim buffer =
- truncate_text buffer max_buffer ;
let p = trim_begin buffer in
let q = trim_end buffer in
p , q
let contents buffer =
- truncate_text buffer max_buffer ; Buffer.contents buffer.content
+ Buffer.contents buffer.content
let message buffer =
( Buffer.contents buffer.content , List.rev buffer.revtags )
@@ -247,7 +243,6 @@ let to_string ?(indent=20) ?(margin=40) ?(trim=true) pp data =
let fmt = formatter buffer in
pp fmt data ;
Format.pp_print_flush fmt () ;
- truncate_text buffer max_buffer ;
if trim then
let p = trim_begin buffer in
let q = trim_end buffer in
diff --git a/src/libraries/utils/rich_text.mli b/src/libraries/utils/rich_text.mli
index 864f9647854cd605373bea71078e3501e95a2189..0290a56ff053ceff3bf8b15d39f052a0cec4d1d0 100644
--- a/src/libraries/utils/rich_text.mli
+++ b/src/libraries/utils/rich_text.mli
@@ -106,6 +106,10 @@ val trim : buffer -> int * int
(** Resize the buffer to roughly fit its actual content. *)
val shrink : buffer -> unit
+(** [truncate buffer size] truncates the content of [buffer] if longer than
+ [size] characters. Returns true if the bufffer has been truncated. *)
+val truncate : buffer -> int -> bool
+
(* -------------------------------------------------------------------------- *)
(** Printer *)
(* -------------------------------------------------------------------------- *)
diff --git a/tests/misc/dune b/tests/misc/dune
index 1ac66020dfef15db60a3f578e47e78b01f746433..04a2773384edb245d309668e598586ab6071a911 100644
--- a/tests/misc/dune
+++ b/tests/misc/dune
@@ -8,3 +8,8 @@
(enabled_if %{bin-available:gcc})
(deps pragma-pack.c pragma-pack-utils.h)
)
+
+(cram
+ (applies_to log-truncation)
+ (enabled_if %{bin-available:socat})
+)
diff --git a/tests/misc/log-truncation.t/dune b/tests/misc/log-truncation.t/dune
new file mode 100644
index 0000000000000000000000000000000000000000..01bb108622d6e01041363964775229012333d218
--- /dev/null
+++ b/tests/misc/log-truncation.t/dune
@@ -0,0 +1,8 @@
+(executable
+ (name "log_truncation")
+ (modules "log_truncation")
+ (modes plugin)
+ (libraries frama-c.init.cmdline frama-c.kernel)
+ (flags -open Frama_c_kernel :standard)
+ (promote (until-clean))
+)
diff --git a/tests/misc/log-truncation.t/dune-project b/tests/misc/log-truncation.t/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..f721e56b4bb4f5de0235f762e96a9f84ebd48f30
--- /dev/null
+++ b/tests/misc/log-truncation.t/dune-project
@@ -0,0 +1,3 @@
+(lang dune 3.13)
+(name frama-c-log-truncation)
+(package (name frama-c-log-truncation))
diff --git a/tests/misc/log-truncation.t/log_truncation.ml b/tests/misc/log-truncation.t/log_truncation.ml
new file mode 100644
index 0000000000000000000000000000000000000000..72a094bcd069acce2cc9bf68b2bbe578c9337f5a
--- /dev/null
+++ b/tests/misc/log-truncation.t/log_truncation.ml
@@ -0,0 +1,13 @@
+let run () =
+ (* This can be filtered to avoid too long test oracles. *)
+ let very_long_line = String.make 5000 '#' in
+ let line = "begin_line <-----" ^ very_long_line ^ "-----> end_line" in
+ let middle_text =
+ "[ This text should only appear in the log if is is redirected to a file. ]"
+ in
+ Kernel.warning
+ "This is a very, very long message intended to test the truncation \
+ of the Frama-C log: \n\
+ @[<v>%s@;%s@;%s@]" line middle_text line
+
+let () = Boot.Main.extend run
diff --git a/tests/misc/log-truncation.t/run.t b/tests/misc/log-truncation.t/run.t
new file mode 100644
index 0000000000000000000000000000000000000000..d3bf022957c6ca38753b4bff9c9c547483a6e303
--- /dev/null
+++ b/tests/misc/log-truncation.t/run.t
@@ -0,0 +1,20 @@
+Compilation of the log_truncation.ml file.
+ $ dune build --cache=disabled --root . _build/default/log_truncation.cmxs
+
+ $ frama-c -no-autoload-plugins -load-module log_truncation.cmxs > file-log.txt
+
+The message should not be truncated as the output was redireted to a file.
+ $ cat file-log.txt | tr -d '#'
+ [kernel] Warning: This is a very, very long message intended to test the truncation of the Frama-C log:
+
+ begin_line <----------> end_line
+ [ This text should only appear in the log if is is redirected to a file. ]
+ begin_line <----------> end_line
+
+ $ socat EXEC:"frama-c -no-autoload-plugins -load-module log_truncation.cmxs",pty GOPEN:terminal-log.txt
+
+The message should be truncated.
+ $ cat terminal-log.txt | tr -d '#'
+ [kernel] Warning: (truncated message) This is a very, very long message intended to test the truncation of the Frama-C log:
+
+ begin_line <-----[...]-----> end_line