diff --git a/src/libraries/utils/markdown.ml b/src/libraries/utils/markdown.ml index d86a51b1f0609a14c851221cd026358ed2bbe890..8d3369239d76b68b864743b132c30e2ab8e418e9 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 7e7047fd73d11a876aaa914bf9d058be12c4f1ba..6cc566b6c573d66cb457d36baae19a85dcc1416e 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 922ec4988e36b72213953e57d5acf5f772994b7a..34ad92040e3f2f5db8d48c4a8028f14c46821f38 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 3a23295f21b117dc05ec53932d8c20860d1ffd5a..44cfad92c9c710f26815ff79bf9ac8ca4afbbd8d 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 385f456c3f75b6f1e424a3a40e8efdd68eb769ad..7ba59f748965cfbbd6de676acedc1af4ff3a6dfe 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); ```