Preparing inclusion of handwritten remarks

src/plugins/markdown-report/Makefile

 FRAMAC_SHARE:=$(shell frama-c -print-share-path)
 
 PLUGIN_NAME:=Report_markdown
-PLUGIN_CMO:=markdown md_gen
+PLUGIN_CMO:=markdown mdr_params parse_remarks md_gen
 PLUGIN_NO_TEST:=true
 
 include $(FRAMAC_SHARE)/Makefile.dynamic
 
-Report_markdown.mli: markdown.mli md_gen.mli
-	echo "module Markdown: sig" > $@
+Report_markdown.mli: mdr_params.mli markdown.mli md_gen.mli Makefile
+	echo "module Mdr_params: sig" > $@
+	cat mdr_params.mli >> $@
+	echo "end" >> $@
+	echo "module Markdown: sig" >> $@
 	cat markdown.mli >> $@
 	echo "end" >> $@
 	echo "module Md_gen: sig" >> $@

src/plugins/markdown-report/Report_markdown.mli

+module Mdr_params: sig
+include Plugin.S
+
+(** Value of [-mdr-out]. *)
+module Output: Parameter_sig.String
+
+(** Value of [-mdr-gen]. *)
+module Generate: Parameter_sig.Bool
+
+(** Value of [-mdr-gen-draft]. *)
+module Gen_draft: Parameter_sig.Bool
+
+(** Value of [-mdr-remarks]. *)
+module Remarks: Parameter_sig.String
+
+(** Value of [-mdr-authors]. *)
+module Authors: Parameter_sig.String_list
+
+(** Value of [-mdr-stubs]. *)
+module Stubs: Parameter_sig.String_list
+end
 module Markdown: sig
 type align = Left | Center | Right
 
@@ -62,17 +83,6 @@ 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

src/plugins/markdown-report/md_gen.ml

 open Cil_types
-
-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 Gen_draft = Self.False(
-  struct
-    let option_name = "-mdr-gen-draft"
-    let help =
-      "instead of a full report, generates an empty draft \
-       in a format suitable for -mdr-add-remarks"
-  end)
-
-module Remarks = Self.Empty_string(
-struct
-  let option_name = "-mdr-remarks"
-  let arg_name = "f"
-  let help =
-    "reads <f> to add additional remarks to various sections of the report. \
-     must be in a format compatible with the file produced by -mdr-gen-draft. \
-     Remarks themselves must be written in pandoc's markdown, although this is \
-     not enforced by the plug-in."
-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 =
@@ -127,7 +70,7 @@ let section_stubs is_draft =
       (List.map
          (fun filename ->
             Globals.FileIndex.get_functions ~declarations:false ~filename)
-         (Stubs.get ())
+         (Mdr_params.Stubs.get ())
       )
   in
   let opt = Dynamic.Parameter.String.get "-val-use-spec" () in
@@ -489,10 +432,18 @@ let gen_section_callgraph is_draft =
   in
   H1 (plain "Flamegraph", Some "flamegraph") :: content
 
+let gen_section_postlude is_draft =
+  if is_draft then
+    [ H1 (plain "Postlude", Some "postlude");
+      Comment "You can put here some concluding remarks" ]
+    @ insert_marks
+  else []
+
 let gen_alarms is_draft =
   gen_section_warnings is_draft @
   gen_section_alarms is_draft @
-  gen_section_callgraph is_draft
+  gen_section_callgraph is_draft @
+  gen_section_postlude is_draft
 
 let mk_date () =
   let tm = Unix.gmtime (Unix.time()) in
@@ -501,7 +452,7 @@ let mk_date () =
        (1900 + tm.Unix.tm_year) (1 + tm.Unix.tm_mon) tm.Unix.tm_mday)
 
 let mk_remarks () =
-  let f = Remarks.get () in
+  let f = Mdr_params.Remarks.get () in
   if f <> "" then failwith "writeme"
   else Datatype.String.Map.empty
 
@@ -512,7 +463,7 @@ let gen_report is_draft =
   let title =
     if is_draft then plain "Frama-C Analysis Report" else plain "Draft report"
   in
-  let authors = List.map (fun x -> plain x) (Authors.get ()) in
+  let authors = List.map (fun x -> plain x) (Mdr_params.Authors.get ()) in
   let date = mk_date () in
   let elements = context @ alarms in
   let elements =
@@ -520,8 +471,11 @@ let gen_report is_draft =
       Comment
         "This file contains additional remarks that will be added to \
          automatically generated content by Frama-C's Markdown-report plugin. \
-         For any section of the document, you can write markdown content \
-         between the BEGIN and END comments. Please don't alter the structure \
+         For any section of the document, you can write pandoc markdown \
+         content between the BEGIN and END comments. In addition, the plug-in \
+         will consider any <!-- INCLUDE file.md --> comment as a directive to \
+         include the content of file.md in the corresponding section. \
+         Please don't alter the structure \
          of the document as it is used by the plugin to associate content to \
          the relevant section."
       :: elements
@@ -529,23 +483,23 @@ let gen_report is_draft =
   in
   let doc = { title; authors; date; elements;} in
   try
-    let out = open_out (Output.get()) in
+    let out = open_out (Mdr_params.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
+    Mdr_params.warning
       "Unable to open %s for writing (%s). No report will be generated"
-      (Output.get()) s
+      (Mdr_params.Output.get()) s
 
 let main () =
-  if Gen_draft.get () then begin
-    if Generate.get () then
-      Self.warning
+  if Mdr_params.Gen_draft.get () then begin
+    if Mdr_params.Generate.get () then
+      Mdr_params.warning
         "-mdr-gen and -mdr-gen-draft can be activated at the \
          same time. Only draft will be generated";
     gen_report true
   end
-  else if Generate.get () then gen_report false
+  else if Mdr_params.Generate.get () then gen_report false
 
 let () = Db.Main.extend main

src/plugins/markdown-report/md_gen.mli

-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

src/plugins/markdown-report/mdr_params.ml

+include Plugin.Register(
+  struct
+    let name = "Markdown report"
+    let shortname = "mdr"
+    let help = "generates a report in markdown format"
+  end)
+
+module Output = 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 = False(
+struct
+  let option_name = "-mdr-gen"
+  let help = "generates an analysis report on the current project"
+end)
+
+module Gen_draft = False(
+  struct
+    let option_name = "-mdr-gen-draft"
+    let help =
+      "instead of a full report, generates an empty draft \
+       in a format suitable for -mdr-add-remarks"
+  end)
+
+module Remarks = Empty_string(
+struct
+  let option_name = "-mdr-remarks"
+  let arg_name = "f"
+  let help =
+    "reads <f> to add additional remarks to various sections of the report. \
+     must be in a format compatible with the file produced by -mdr-gen-draft. \
+     Remarks themselves must be written in pandoc's markdown, although this is \
+     not enforced by the plug-in."
+end
+)
+
+module Authors = String_list(
+struct
+  let option_name = "-mdr-authors"
+  let arg_name = "l"
+  let help = "list of authors of the report"
+end)
+
+module Stubs = String_list(
+  struct
+    let option_name = "-mdr-stubs"
+    let arg_name = "f1,...,fn"
+    let help = "list of C files containing stub functions"
+  end)

src/plugins/markdown-report/mdr_params.mli

+include Plugin.S
+
+(** Value of [-mdr-out]. *)
+module Output: Parameter_sig.String
+
+(** Value of [-mdr-gen]. *)
+module Generate: Parameter_sig.Bool
+
+(** Value of [-mdr-gen-draft]. *)
+module Gen_draft: Parameter_sig.Bool
+
+(** Value of [-mdr-remarks]. *)
+module Remarks: Parameter_sig.String
+
+(** Value of [-mdr-authors]. *)
+module Authors: Parameter_sig.String_list
+
+(** Value of [-mdr-stubs]. *)
+module Stubs: Parameter_sig.String_list

src/plugins/markdown-report/parse_remarks.ml

+type env =
+  { mutable current_section: string;
+    mutable is_markdown: bool;
+    current_markdown: Buffer.t;
+    mutable remarks: Markdown.element list Datatype.String.Map.t }
+
+let empty_env () =
+  { current_section = "";
+    is_markdown = false;
+    current_markdown = Buffer.create 40;
+    remarks = Datatype.String.Map.empty }
+
+let add_channel buf chan =
+  try
+    while true do
+      let s = input_line chan in
+      Buffer.add_string buf s;
+      Buffer.add_char buf '\n'
+    done;
+  with End_of_file -> ()
+
+let end_markdown = Str.regexp_string "<!-- BEGIN_REMARK -->"
+
+let beg_markdown = Str.regexp_string "<!-- END_REMARK -->"
+
+let include_markdown = Str.regexp "<!-- INCLUDE \\(.*\\) -->"
+
+let is_section = Str.regexp "^#[^{]{\\([^}]*\\)}"
+
+let parse_line env line =
+  if env.is_markdown then begin
+    if Str.string_match end_markdown line 0 then begin
+      env.remarks <-
+        Datatype.String.Map.add
+          env.current_section
+          [ Markdown.Raw (Buffer.contents env.current_markdown)]
+          env.remarks
+    end else if Str.string_match include_markdown line 0 then begin
+      let f = Str.matched_group 1 line in
+      try
+        let chan = open_in f in
+        add_channel env.current_markdown chan;
+        close_in chan
+      with Sys_error err ->
+        Mdr_params.error
+          "Unable to open included remarks file %s (%s), Ignoring." f err
+    end else begin
+      Buffer.add_string env.current_markdown line;
+      Buffer.add_char env.current_markdown '\n'
+    end
+  end else if Str.string_match beg_markdown line 0 then begin
+    env.is_markdown <- true
+  end else if Str.string_match is_section line 0 then begin
+    let sec = Str.matched_group 1 line in
+    env.current_section <- sec
+  end
+
+let parse_remarks env chan =
+  try
+    while true do
+      let s = input_line chan in
+      parse_line env s
+    done;
+    assert false
+  with End_of_file ->
+    close_in chan;
+    env
+
+let get_remarks f =
+  try
+    let chan = open_in f in
+    let { remarks } = parse_remarks (empty_env ()) chan in
+    remarks
+  with Sys_error err ->
+    Mdr_params.error
+      "Unable to open remarks file %s (%s). \
+       No additional remarks will be included in the report." f err;
+    Datatype.String.Map.empty

src/plugins/markdown-report/parse_remarks.mli

+(** Parse skeleton files to add manually written comments to various parts
+    of the report. *)
+
+(** [get_remarks f] retrieves the elements associated to various sections
+    of the report, referenced by their anchor. *)
+val get_remarks: string -> Markdown.element list Datatype.String.Map.t