From b114f58d8fed8556ca8f39b62ff5c675f5a07435 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 28 Oct 2019 12:17:21 +0100
Subject: [PATCH] [markdown] refactor codeblock smart-constructor
---
src/libraries/utils/markdown.ml | 16 ++++++++++++----
src/libraries/utils/markdown.mli | 9 +++++----
src/plugins/markdown-report/md_gen.ml | 8 ++++----
src/plugins/markdown-report/sarif_gen.ml | 2 +-
.../markdown-report/tests/eva/oracle/cwe126.0.md | 4 ++--
5 files changed, 24 insertions(+), 15 deletions(-)
diff --git a/src/libraries/utils/markdown.ml b/src/libraries/utils/markdown.ml
index d86a51b1f06..8d3369239d7 100644
--- a/src/libraries/utils/markdown.ml
+++ b/src/libraries/utils/markdown.ml
@@ -119,10 +119,18 @@ let link ?text ?page ?name () =
| None, Some a -> Section("",a)
| Some p, Some a -> Section(p,a)
-let codeblock lang pp code =
- let s = Format.asprintf "@[%a@]" pp code in
- let lines = String.split_on_char '\n' s in
- [Code_block (lang, lines)]
+let codeblock ?(lang="") content =
+ let buffer = Buffer.create 120 in
+ let fmt = Format.formatter_of_buffer buffer in
+ Format.pp_open_hvbox fmt 0 ;
+ Format.kfprintf
+ (fun fmt ->
+ Format.pp_close_box fmt () ;
+ Format.pp_print_flush fmt () ;
+ let code = Buffer.contents buffer |> String.trim in
+ let lines = String.split_on_char '\n' code in
+ [Code_block(lang,lines)]
+ ) fmt content
let text text = [Text text]
let list items = [UL items]
diff --git a/src/libraries/utils/markdown.mli b/src/libraries/utils/markdown.mli
index 7e7047fd73d..6cc566b6c57 100644
--- a/src/libraries/utils/markdown.mli
+++ b/src/libraries/utils/markdown.mli
@@ -146,10 +146,11 @@ val enum : block list -> block
(** Description list *)
val description : (text * text) list -> block
-(** [codeblock lang pp code] returns a [Code_block] for [code],
- written in [lang], as pretty-printed by [pp]. *)
-val codeblock:
- string -> (Format.formatter -> 'a -> unit) -> 'a -> block
+(** [codeblock lang "...."] returns a [Code_block] for [code],
+ written in [lang] with the given formatted content.
+ The code block content placed inside an englobing hv-box, trimed
+ and finally splitted into lines. *)
+val codeblock : ?lang:string -> ('a,Format.formatter,unit,block) format4 -> 'a
(** {2 Document Elements}
diff --git a/src/plugins/markdown-report/md_gen.ml b/src/plugins/markdown-report/md_gen.ml
index 922ec4988e3..34ad92040e3 100644
--- a/src/plugins/markdown-report/md_gen.ml
+++ b/src/plugins/markdown-report/md_gen.ml
@@ -134,7 +134,7 @@ let section_stubs env =
else
let intro = Markdown.text @@ Markdown.format
"`%s` has the following specification" s in
- let funspec = Markdown.codeblock "acsl"
+ let funspec = Markdown.codeblock ~lang:"acsl" "%a"
Printer.pp_funspec (Annotations.funspec kf) in
Block ( intro @ funspec ) :: insert_remark env anchor
in
@@ -151,7 +151,7 @@ let section_stubs env =
let intro = Markdown.text @@ Markdown.format
"`%s` @[<h>is defined at %a@]"
name Cil_datatype.Location.pretty loc in
- let fundecl = Markdown.codeblock "c"
+ let fundecl = Markdown.codeblock ~lang:"c" "%a"
Printer.pp_global (GFun (Kernel_function.get_definition kf,loc)) in
Block ( intro @ fundecl ) :: insert_remark env anchor
in
@@ -373,7 +373,7 @@ let section_event is_err env nb event =
H2 (plain title, Some lab)
:: Block (
(text @@ plain "Message:") @
- codeblock "log" Format.pp_print_string event.evt_message
+ codeblock "[%s] %s" event.evt_plugin event.evt_message
)
:: content
@@ -461,7 +461,7 @@ let gen_section_alarms env =
let loc = string_of_loc @@ Cil_datatype.Stmt.loc s in
let loc_text = plain loc in
let emitter = code (Emitter.get_name e) in
- let descr = codeblock "acsl" Printer.pp_code_annotation annot in
+ let descr = codeblock ~lang:"acsl" "%a" Printer.pp_code_annotation annot in
let sec_title = format "Alarm %d at %s" i loc in
let sec_content =
if env.is_draft then
diff --git a/src/plugins/markdown-report/sarif_gen.ml b/src/plugins/markdown-report/sarif_gen.ml
index 3a23295f21b..44cfad92c9c 100644
--- a/src/plugins/markdown-report/sarif_gen.ml
+++ b/src/plugins/markdown-report/sarif_gen.ml
@@ -87,7 +87,7 @@ let make_message alarm annot remark =
let name = Alarms.get_name alarm in
let text = name ^ "." in
let kind = plain (name ^ ":") in
- let descr = codeblock "acsl" Printer.pp_code_annotation annot in
+ let descr = codeblock ~lang:"acsl" "%a" Printer.pp_code_annotation annot in
let summary = Block (Text kind :: descr) in
let markdown =
match remark with
diff --git a/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md b/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md
index 385f456c3f7..7ba59f74896 100644
--- a/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md
+++ b/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md
@@ -67,8 +67,8 @@ Table: Warning reported by Frama-C
Message:
-```log
-out of bounds read. assert \valid_read(data + i);
+```
+[eva] out of bounds read. assert \valid_read(data + i);
```
--
GitLab