diff --git a/src/plugins/markdown-report/Makefile b/src/plugins/markdown-report/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..a25ff70a96c64c6aeb60e161c13e7029830ba0fd
--- /dev/null
+++ b/src/plugins/markdown-report/Makefile
@@ -0,0 +1,15 @@
+FRAMAC_SHARE:=$(shell frama-c -print-share-path)
+
+PLUGIN_NAME:=Report_markdown
+PLUGIN_CMO:=markdown md_gen
+PLUGIN_NO_TEST:=true
+
+include $(FRAMAC_SHARE)/Makefile.dynamic
+
+Report_markdown.mli: markdown.mli md_gen.mli
+ echo "module Markdown: sig" > $@
+ cat markdown.mli >> $@
+ echo "end" >> $@
+ echo "module Md_gen: sig" >> $@
+ cat md_gen.mli >> $@
+ echo "end" >> $@
diff --git a/src/plugins/markdown-report/README.md b/src/plugins/markdown-report/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..0b42fe16fbbefc12183f71b77601f567e686d26e
--- /dev/null
+++ b/src/plugins/markdown-report/README.md
@@ -0,0 +1,4 @@
+Generation of pandoc reports.
+
+**Important Note:** Requires OCaml 4.04 or newer (uses a new function from
+`String`), instead of the normal 4.02.3 or newer for Frama-C kernel.
diff --git a/src/plugins/markdown-report/Report_markdown.mli b/src/plugins/markdown-report/Report_markdown.mli
new file mode 100644
index 0000000000000000000000000000000000000000..c5b9481ff9db5e0fa1151772c85572e22fd79958
--- /dev/null
+++ b/src/plugins/markdown-report/Report_markdown.mli
@@ -0,0 +1,75 @@
+module Markdown: sig
+type align = Left | Center | Right
+
+type inline =
+ | Plain of string
+ | Emph of string
+ | Bold of string
+ | Inline_code of string
+ | Link of text * string (** [Link(text,url)] *)
+ | Image of string * string (** [Image(alt,location)] *)
+
+and text = inline list
+
+type block_element =
+ | Text of text (** single paragraph of text. *)
+ | Block_quote of element list
+ | UL of block list
+ | OL of block list
+ | DL of (text * text) list (** definition list *)
+ | EL of (string option * text) list (** example list *)
+ | Code_block of string * string list
+
+and block = block_element list
+
+and element =
+ | Block of block
+ | Raw of string (** non-markdown element, printed as-is. *)
+ | H1 of text * string option (** optional label. *)
+ | H2 of text * string option
+ | H3 of text * string option
+ | H4 of text * string option
+ | H5 of text * string option
+ | H6 of text * string option
+ | Table of { caption: text option; header: (text * align) list;
+ content: text list list; }
+
+type pandoc_markdown =
+ { title: text;
+ authors: text list;
+ date: text;
+ elements: element list
+ }
+
+val plain: string -> text
+
+(** gives a link whose text is the URL itself. *)
+val plain_link: string -> inline
+
+val pp_inline: Format.formatter -> inline -> unit
+
+val pp_text: Format.formatter -> text -> unit
+
+val pp_block_element: Format.formatter -> block_element -> unit
+
+val pp_block: Format.formatter -> block -> unit
+
+val pp_element: Format.formatter -> element -> unit
+
+val pp_pandoc: Format.formatter -> pandoc_markdown -> unit
+end
+module Md_gen: sig
+module Self: Plugin.S
+
+(** state of [-mdr-out] option *)
+module Output: Parameter_sig.String
+
+(** state of [-mdr-generate] option *)
+module Generate: Parameter_sig.Bool
+
+(** state of [-mdr-authors] option *)
+module Authors: Parameter_sig.String_list
+
+(** generates the report. *)
+val main: unit -> unit
+end
diff --git a/src/plugins/markdown-report/markdown.ml b/src/plugins/markdown-report/markdown.ml
new file mode 100644
index 0000000000000000000000000000000000000000..19a1f5032777d6091b7e777634320bc7ae3ff9e1
--- /dev/null
+++ b/src/plugins/markdown-report/markdown.ml
@@ -0,0 +1,200 @@
+type align = Left | Center | Right
+
+type inline =
+ | Plain of string
+ | Emph of string
+ | Bold of string
+ | Inline_code of string
+ | Link of text * string (** [Link(text,url)] *)
+ | Image of string * string (** [Image(alt,location)] *)
+
+and text = inline list
+
+type block_element =
+ | Text of text (** single paragraph of text. *)
+ | Block_quote of element list
+ | UL of block list
+ | OL of block list
+ | DL of (text * text) list (** definition list *)
+ | EL of (string option * text) list (** example list *)
+ | Code_block of string * string list
+
+and block = block_element list
+
+and element =
+ | Block of block
+ | Raw of string (** non-markdown element, printed as-is. *)
+ | H1 of text * string option (** optional label. *)
+ | H2 of text * string option
+ | H3 of text * string option
+ | H4 of text * string option
+ | H5 of text * string option
+ | H6 of text * string option
+ | Table of { caption: text option; header: (text * align) list;
+ content: text list list; }
+
+type pandoc_markdown =
+ { title: text;
+ authors: text list;
+ date: text;
+ elements: element list
+ }
+
+let plain s = [ Plain s]
+
+let plain_link s = Link ([Inline_code s],s)
+
+let rec pp_inline fmt =
+ function
+ | Plain s -> Format.pp_print_string fmt s
+ | Emph s -> Format.fprintf fmt "_%s_" (String.trim s)
+ | Bold s -> Format.fprintf fmt "**%s**" (String.trim s)
+ | Inline_code s -> Format.fprintf fmt "`%s`" (String.trim s)
+ | Link (text,url) -> Format.fprintf fmt "@[<h>[%a](%s)@]@ " pp_text text url
+ | Image (alt,url) -> Format.fprintf fmt "@[<h>@]@ " alt url
+
+and pp_text fmt l =
+ match l with
+ | [] -> ()
+ | [ elt ] -> pp_inline fmt elt
+ | elt :: text -> Format.fprintf fmt "%a@ %a" pp_inline elt pp_text text
+
+let pp_lab fmt = function
+ | None -> ()
+ | Some lab -> Format.fprintf fmt " {#%s}" lab
+
+let test_size txt = String.length (Format.asprintf "%a" pp_text txt)
+
+let pp_dashes fmt size =
+ let dashes = String.make (size + 2) '-' in
+ Format.fprintf fmt "%s+" dashes
+
+let pp_sep_line fmt sizes =
+Format.fprintf fmt "@[<h>+";
+List.iter (pp_dashes fmt) sizes;
+Format.fprintf fmt "@]@\n"
+
+let pp_header fmt (t,_) size =
+ let real_size = test_size t in
+ let spaces = String.make (size - real_size) ' ' in
+ Format.fprintf fmt " %a%s |" pp_text t spaces
+
+let pp_headers fmt l sizes =
+ Format.fprintf fmt "@[<h>|";
+ List.iter2 (pp_header fmt) l sizes;
+ Format.fprintf fmt "@]@\n"
+
+let compute_sizes headers contents =
+ let check_line i m line =
+ match List.nth_opt line i with
+ | Some t -> max m (test_size t + 2)
+ | None -> m
+ in
+ let column_size (i,l) (h,_) =
+ let max = List.fold_left (check_line i) (test_size h) contents in
+ (i+1, max :: l)
+ in
+ let (_,sizes) = List.fold_left column_size (0,[]) headers in
+ List.rev sizes
+
+let pp_align fmt align size =
+ let sep = String.make size '=' in
+ match align with
+ | (_,Left) -> Format.fprintf fmt ":%s=+" sep
+ | (_,Center) -> Format.fprintf fmt ":%s:+" sep
+ | (_,Right) -> Format.fprintf fmt "%s=:+" sep
+
+let pp_aligns fmt headers sizes =
+ Format.fprintf fmt "@[<h>+";
+ List.iter2 (pp_align fmt) headers sizes;
+ Format.fprintf fmt "@]@\n"
+
+let pp_table_cell fmt size t =
+ let real_size = test_size t in
+ let spaces = String.make (size - real_size) ' ' in
+ Format.fprintf fmt " %a%s |" pp_text t spaces
+
+let pp_table_line fmt sizes l =
+ Format.fprintf fmt "@[<h>|";
+ List.iter2 (pp_table_cell fmt) sizes l;
+ Format.fprintf fmt "@]@\n";
+ pp_sep_line fmt sizes
+
+let pp_table_content fmt l sizes =
+ Format.fprintf fmt "@[<v>";
+ List.iter (pp_table_line fmt sizes) l;
+ Format.fprintf fmt "@]@\n"
+
+let rec pp_block_element fmt = function
+ | Text t -> Format.fprintf fmt "@[<hov>%a@]@\n" pp_text t
+ | Block_quote l -> pp_quote fmt l
+ | UL l -> pp_list "*" fmt l
+ | OL l -> pp_list "#." fmt l
+ | DL l ->
+ List.iter
+ (fun (term,def) ->
+ Format.fprintf fmt "@[<h>%a@]@\n@\n@[<hov 2>: %a@]@\n@\n"
+ pp_text term pp_text def)
+ l
+ | EL l ->
+ List.iter
+ (fun (lab,txt) ->
+ match lab with
+ | None -> Format.fprintf fmt "@[<hov 4>(@@) %a@]@\n" pp_text txt
+ | Some s -> Format.fprintf fmt "@[<hov 4>(@@%s) %a@]@\n" s pp_text txt)
+ l
+ | Code_block (language, lines) ->
+ Format.fprintf fmt "@[<h>```%s@]@\n" language;
+ List.iter (fun line -> Format.fprintf fmt "@[<h>%s@]@\n" line) lines;
+ Format.fprintf fmt "```@\n"
+
+and pp_list prefix fmt l =
+ List.iter
+ (fun item ->
+ Format.fprintf fmt "@[<v 4>@[<hov>%s %a@]@]" prefix pp_block item)
+ l
+
+and pp_block fmt l =
+ match l with
+ | [ elt ] -> pp_block_element fmt elt
+ | _ ->
+ Format.fprintf fmt "%a@\n"
+ (Format.pp_print_list ~pp_sep:Format.pp_force_newline pp_block_element) l
+
+and pp_quote fmt l =
+ List.iter
+ (fun elt -> Format.fprintf fmt "@[<v>> %a@]" pp_element elt) l
+
+and pp_element fmt = function
+ | Block b -> Format.fprintf fmt "@[<v>%a@]@\n" pp_block b
+ | Raw s -> Format.pp_print_string fmt s
+ | H1(t,lab) -> Format.fprintf fmt "@[<h># %a%a@]@\n" pp_text t pp_lab lab
+ | H2(t,lab) -> Format.fprintf fmt "@[<h>## %a%a@]@\n" pp_text t pp_lab lab
+ | H3(t,lab) -> Format.fprintf fmt "@[<h>### %a%a@]@\n" pp_text t pp_lab lab
+ | H4(t,lab) -> Format.fprintf fmt "@[<h>#### %a%a@]@\n" pp_text t pp_lab lab
+ | H5(t,lab) -> Format.fprintf fmt "@[<h>##### %a%a@]@\n" pp_text t pp_lab lab
+ | H6(t,lab) -> Format.fprintf fmt "@[<h>###### %a%a@]@\n" pp_text t pp_lab lab
+ | Table { caption; header; content } ->
+ (match caption with
+ | None -> ()
+ | Some t -> Format.fprintf fmt "@[<h>Table: %a@]@\n@\n" pp_text t);
+ let sizes = compute_sizes header content in
+ pp_sep_line fmt sizes;
+ pp_headers fmt header sizes;
+ pp_aligns fmt header sizes;
+ pp_table_content fmt content sizes
+
+let pp_authors fmt l =
+ List.iter (fun t -> Format.fprintf fmt "@[<h>- %a@]@\n" pp_text t) l
+
+let pp_pandoc fmt { title; authors; date; elements } =
+ Format.fprintf fmt "@[<v>";
+ if title <> [] || authors <> [] || date <> [] then begin
+ Format.fprintf fmt "@[<h>---@]@\n";
+ Format.fprintf fmt "@[<h>title: %a@]@\n" pp_text title;
+ Format.fprintf fmt "@[<h>author:@]@\n%a" pp_authors authors;
+ Format.fprintf fmt "@[<h>date: %a@]@\n" pp_text date;
+ Format.fprintf fmt "@[<h>...@]@\n";
+ end;
+ List.iter (pp_element fmt) elements;
+ Format.fprintf fmt "@]%!"
diff --git a/src/plugins/markdown-report/markdown.mli b/src/plugins/markdown-report/markdown.mli
new file mode 100644
index 0000000000000000000000000000000000000000..e8a0a8c797b8fd3f175fe0acdc9211f7ead43310
--- /dev/null
+++ b/src/plugins/markdown-report/markdown.mli
@@ -0,0 +1,58 @@
+type align = Left | Center | Right
+
+type inline =
+ | Plain of string
+ | Emph of string
+ | Bold of string
+ | Inline_code of string
+ | Link of text * string (** [Link(text,url)] *)
+ | Image of string * string (** [Image(alt,location)] *)
+
+and text = inline list
+
+type block_element =
+ | Text of text (** single paragraph of text. *)
+ | Block_quote of element list
+ | UL of block list
+ | OL of block list
+ | DL of (text * text) list (** definition list *)
+ | EL of (string option * text) list (** example list *)
+ | Code_block of string * string list
+
+and block = block_element list
+
+and element =
+ | Block of block
+ | Raw of string (** non-markdown element, printed as-is. *)
+ | H1 of text * string option (** optional label. *)
+ | H2 of text * string option
+ | H3 of text * string option
+ | H4 of text * string option
+ | H5 of text * string option
+ | H6 of text * string option
+ | Table of { caption: text option; header: (text * align) list;
+ content: text list list; }
+
+type pandoc_markdown =
+ { title: text;
+ authors: text list;
+ date: text;
+ elements: element list
+ }
+
+val plain: string -> text
+
+(** gives a link whose text is the URL itself. *)
+val plain_link: string -> inline
+
+val pp_inline: Format.formatter -> inline -> unit
+
+val pp_text: Format.formatter -> text -> unit
+
+val pp_block_element: Format.formatter -> block_element -> unit
+
+val pp_block: Format.formatter -> block -> unit
+
+val pp_element: Format.formatter -> element -> unit
+
+val pp_pandoc: Format.formatter -> pandoc_markdown -> unit
diff --git a/src/plugins/markdown-report/md_gen.ml b/src/plugins/markdown-report/md_gen.ml
new file mode 100644
index 0000000000000000000000000000000000000000..d2fff1bc6278c657aca86d0ff9d5dd14cda3c11f
--- /dev/null
+++ b/src/plugins/markdown-report/md_gen.ml
@@ -0,0 +1,380 @@
+module Self =
+ Plugin.Register(
+ struct
+ let name = "Markdown report"
+ let shortname = "mdr"
+ let help = "generates a report in markdown format"
+ end)
+
+module Output = Self.String(
+struct
+ let option_name = "-mdr-out"
+ let arg_name = "f"
+ let default = "report.md"
+ let help = "sets the name of the output file to <f>"
+end)
+
+module Generate = Self.False(
+struct
+ let option_name = "-mdr-gen"
+ let help = "generates an analysis report on the current project"
+end)
+
+module Authors = Self.String_list(
+struct
+ let option_name = "-mdr-authors"
+ let arg_name = "l"
+ let help = "list of authors of the report"
+end)
+
+module Stubs = Self.String_list(
+ struct
+ let option_name = "-mdr-stubs"
+ let arg_name = "f1,...,fn"
+ let help = "list of C files containing stub functions"
+ end)
+
+open Markdown
+
+let all_eva_domains =
+ [ "-eva-apron-box", "box domain of the Apron library";
+ "-eva-apron-oct", "octagon domain of the Apron library";
+ "-eva-bitwise-domain", "domain for bitwise computations";
+ "-eva-equality-domain",
+ "domain for storing equalities between memory locations";
+ "-eva-gauges-domain",
+ "gauges domain for relations between memory locations and loop counter";
+ "-eva-inout-domain",
+ "domain for input and output memory locations";
+ "-eva-polka-equalities",
+ "linear equalities domain of the Apron library";
+ "-eva-polka-loose",
+ "loose polyhedra domain of the Apron library";
+ "-eva-polka-strict",
+ "strict polyhedra domain of the Apron library";
+ "-eva-sign-domain", "sign domain (useful only for demos)";
+ "-eva-symbolic-locations-domain",
+ "domain computing ranges of variation for symbolic locations \
+ (e.g. `a[i]` when `i` is not precisely known by `Cvalue`)"
+]
+
+let plural l s =
+ match l with
+ | [] | [ _ ] -> s
+ | _::_::_ -> s ^ "s"
+
+let get_eva_domains () =
+ Extlib.filter_map
+ (fun (x,_) -> Dynamic.Parameter.Bool.get x ())
+ (fun (x,y) -> ([Plain "option"; Inline_code x], plain y))
+ all_eva_domains
+
+let codelines 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 section_domains () =
+ let l = get_eva_domains () in
+ Block
+ (match l with
+ | [] ->
+ [Text
+ (plain
+ "Only the base domain (`Cvalue`) has been used for the analysis")]
+ | _ ->
+ [Text
+ (plain
+ "In addition to the base domain (`Cvalue`), additional domains \
+ have been used by EVA");
+ DL l]
+ )
+
+let section_stubs () =
+ let stubbed_kf =
+ List.concat
+ (List.map
+ (fun filename ->
+ Globals.FileIndex.get_functions ~declarations:false ~filename)
+ (Stubs.get ())
+ )
+ in
+ let opt = Dynamic.Parameter.String.get "-val-use-spec" () in
+ (* NB: requires OCaml >= 4.04 *)
+ let l = String.split_on_char ',' opt in
+ let use_spec =
+ Extlib.filter_map
+ (* The option can include categories in Frama-C's List/Set/Map sense,
+ which begins with a '@'. In particular, @default is included by
+ default. Theoretically, there could also be some '-' to suppress
+ the inclusion of a function
+ *)
+ (fun s -> String.length s <> 0 && s.[0] <> '@' && s.[0] <> '-')
+ (fun s ->
+ let kf = Globals.Functions.find_by_name s in
+ [ Text [Inline_code s; Plain "with the following specification"];
+ codelines "acsl" Printer.pp_funspec (Annotations.funspec kf)])
+ l
+ in
+ let describe_func kf =
+ [Text
+ [ Inline_code (Kernel_function.get_name kf);
+ Plain
+ (Format.asprintf
+ "@[<h>(defined at %a)@]"
+ Cil_datatype.Location.pretty
+ (Kernel_function.get_location kf))
+ ]]
+ in
+ let content =
+ if stubbed_kf <> [] then begin
+ [ Text
+ (plain
+ "The following functions have been stubbed with a C definition");
+ UL (List.map describe_func stubbed_kf)]
+ end else []
+ in
+ let content =
+ if use_spec <> [] then begin
+ [ Text
+ (plain
+ "The following functions have been stubbed with an \
+ ACSL specification");
+ UL use_spec]
+ end else content
+ in
+ if content = [] then
+ Block [Text (plain "No stubs have been used for this analysis")]
+ else
+ Block content
+
+let gen_context () = [
+ H1 (plain "Context of the analysis", Some "context");
+ H2 (plain "Input files", Some "c-input");
+ Block [
+ Text
+ (plain "The C source files (not including the headers `.h` files)" @
+ plain "that have been considered during the analysis are the following:"
+ );
+ UL (List.map (fun x -> [Text [ Inline_code x ]]) (Kernel.Files.get ()));
+ ];
+ H2 (plain "Configuration", Some "options");
+ Block [
+ Text
+ (plain "The options that have been used for this analysis \
+ are the following.")];
+ H3 (plain "EVA Domains", Some "domains");
+ section_domains();
+ H3 (plain "Stubbed Functions", Some "stubs");
+ section_stubs()
+]
+
+let make_events_table print_kind caption events =
+ let open Log in
+ let caption = Some caption in
+ let header =
+ [
+ plain "Location", Left;
+ plain "Description", Left;
+ ]
+ in
+ let header =
+ if print_kind then (plain "Kind", Center) :: header else header
+ in
+ let kind = function
+ | Result -> "Result"
+ | Feedback -> "Feedback"
+ | Debug -> "Debug"
+ | Warning -> "Warning"
+ | Error -> "User error"
+ | Failure -> "Internal error"
+ in
+ let pos = function
+ | None -> "Global"
+ | Some pos ->
+ Format.asprintf
+ "%s:%d" (Filename.basename pos.Lexing.pos_fname) pos.Lexing.pos_lnum
+ in
+ let treat_event { evt_kind; evt_plugin; evt_source; evt_message } =
+ let evt_message =
+ Str.global_replace (Str.regexp_string "\n") " " evt_message
+ in
+ let line =
+ [ plain (pos evt_source);
+ [ Plain evt_message;
+ Plain "(emitted by";
+ Inline_code evt_plugin;
+ Plain ")"
+ ]
+ ]
+ in
+ if print_kind then plain (kind evt_kind) :: line else line
+ in
+ let content = List.fold_left (fun l evt -> treat_event evt :: l) [] events in
+ Table { caption; header; content }
+
+let make_errors_table errs =
+ make_events_table true
+ (plain (plural errs "Error" ^ " reported by Frama-C")) errs
+
+let make_warnings_table warnings =
+ make_events_table
+ false (plain (plural warnings "Warning" ^ " reported by Frama-C")) warnings
+
+let gen_section_warnings () =
+ let open Log in
+ Messages.reset_once_flag ();
+ let errs = ref [] in
+ let warnings = ref [] in
+ let add_event evt =
+ match evt.evt_kind with
+ | Error | Failure -> errs:= evt :: !errs
+ | Warning -> warnings := evt :: !warnings
+ | _ -> ()
+ in
+ Messages.iter add_event;
+ let errs = !errs in
+ let warnings = !warnings in
+ let error_section =
+ if Messages.nb_errors () <> 0 then begin
+ (* Failure are supposed to stop the analyses right away, so that no
+ report will be generated. On the other hand, Error messages can be
+ triggered without stopping everything. Applying the same treatment
+ to a Failure catched by an evil plugin cannot hurt.
+ *)
+ [ H1 (plain "Errors in the analyzer", Some "errors");
+ Block [
+ Text [Bold "Important warning:";
+ Plain "Frama-C did not complete its execution successfully.";
+ Plain "Analysis results may be inaccurate.";
+ Plain ((plural errs "The error") ^ " listed below must be");
+ Plain "fixed first before examining other warnings and alarms."
+ ];
+ ];
+ make_errors_table errs
+ ]
+ end else []
+ in
+ if Messages.nb_warnings () <> 0 then begin
+ error_section @
+ [ H1 (plain "Warnings", Some "warnings");
+ Block [
+ Text [
+ Plain ("The table below lists the " ^ plural warnings "warning");
+ Plain "that have been emitted by the analyzer.";
+ Plain "They might put additional assumptions on the relevance";
+ Plain "of the analysis results and must be reviewed carefully";
+ ];
+ Text [
+ Plain "Note that this does not take into account emitted alarms:";
+ Plain "they are reported in";
+ Link (plain "in the next section", "#alarms")
+ ]
+ ];
+ make_warnings_table warnings
+ ]
+ end else error_section
+
+let gen_section_alarms () =
+ let treat_alarm e kf s ~rank:_ alarm annot l =
+ let kind = plain (Alarms.get_name alarm) in
+ let func = plain (Kernel_function.get_name kf) in
+ let loc =
+ plain
+ (Format.asprintf
+ "%a" Cil_datatype.Location.pretty (Cil_datatype.Stmt.loc s))
+ in
+ let emitter = plain (Emitter.get_name e) in
+ let descr =
+ [ Inline_code(Format.asprintf "%a" Printer.pp_code_annotation annot)]
+ in
+ [ kind; emitter; func; loc; descr ] :: l
+ in
+ let content = Alarms.fold treat_alarm [] in
+ match content with
+ | [] ->
+ [ H1 (plain "Results of the analysis", Some "alarms");
+ Block [
+ Text
+ [ Bold "No alarm"; Plain "was found during the analysis";
+ Plain "Any execution starting from";
+ Inline_code (Kernel.MainFunction.get_function_name ());
+ Plain "in a context matching the one used for the analysis";
+ Plain "will be immune from any undefined behavior."
+ ]
+ ]
+ ]
+ | _ :: l ->
+ let alarm = if l = [] then "alarm" else "alarms" in
+ let caption =
+ Some (plain (String.capitalize_ascii alarm ^ " emitted by the analysis"))
+ in
+ let header =
+ [ plain "Kind", Center;
+ plain "Emitter", Center;
+ plain "Function", Left;
+ plain "Location", Left;
+ plain "Description", Left;
+ ]
+ in
+ [ H1 (plain "Results of the analysis", Some "alarms");
+ Block [
+ Text
+ [ Plain ("The table below lists the " ^ alarm);
+ Plain "that have been emitted during the analysis.";
+ Plain "Any execution starting from";
+ Inline_code (Kernel.MainFunction.get_function_name());
+ Plain "in a context matching the one used for the analysis";
+ Plain "will be immune from any other undefined behavior."
+ ]
+ ];
+ Table { content; caption; header }
+ ]
+
+let gen_section_callgraph () =
+ [ H1 (plain "Flamegraph", Some "flamegraph");
+ Block [
+ Text [
+ Plain "The image below shows the flamegraph (";
+ plain_link "http://www.brendangregg.com/flamegraphs.html";
+ Plain ") for the chosen entry point."
+ ]
+ ];
+ Block
+ [ Text [Image ("flamegraph", "../server.flamegraph.svg")] ]
+ ]
+
+let gen_alarms () =
+ gen_section_warnings () @
+ gen_section_alarms () @
+ gen_section_callgraph ()
+
+let mk_date () =
+ let tm = Unix.gmtime (Unix.time()) in
+ plain
+ (Printf.sprintf "%d-%02d-%02d"
+ (1900 + tm.Unix.tm_year) (1 + tm.Unix.tm_mon) tm.Unix.tm_mday)
+
+let main () =
+ if Generate.get () then begin
+ let context = gen_context () in
+ let alarms = gen_alarms () in
+ let doc =
+ { title = plain "Frama-C Analysis Report";
+ authors = List.map (fun x -> plain x) (Authors.get ());
+ date = mk_date ();
+ elements = context @ alarms
+ }
+ in
+ try
+ let out = open_out (Output.get()) in
+ let fmt = Format.formatter_of_out_channel out in
+ Markdown.pp_pandoc fmt doc;
+ close_out out
+ with Sys_error s ->
+ Self.warning
+ "Unable to open %s for writing (%s). No report will be generated"
+ (Output.get()) s
+ end
+
+let () = Db.Main.extend main
diff --git a/src/plugins/markdown-report/md_gen.mli b/src/plugins/markdown-report/md_gen.mli
new file mode 100644
index 0000000000000000000000000000000000000000..2e5bd59892e21acccde23b13c695ea7e6a3b22d5
--- /dev/null
+++ b/src/plugins/markdown-report/md_gen.mli
@@ -0,0 +1,13 @@
+module Self: Plugin.S
+
+(** state of [-mdr-out] option *)
+module Output: Parameter_sig.String
+
+(** state of [-mdr-generate] option *)
+module Generate: Parameter_sig.Bool
+
+(** state of [-mdr-authors] option *)
+module Authors: Parameter_sig.String_list
+
+(** generates the report. *)
+val main: unit -> unit