diff --git a/src/plugins/markdown-report/Makefile b/src/plugins/markdown-report/Makefile
index a25ff70a96c64c6aeb60e161c13e7029830ba0fd..ed8faa6186fc44f87fe97f08a8f2f8642f25a5dc 100644
--- a/src/plugins/markdown-report/Makefile
+++ b/src/plugins/markdown-report/Makefile
@@ -1,13 +1,16 @@
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" >> $@
diff --git a/src/plugins/markdown-report/Report_markdown.mli b/src/plugins/markdown-report/Report_markdown.mli
index 528de49a885a13546f78a395c542ced38397292a..5f38b40b369bc01929f1b544836795f2e5b55057 100644
--- a/src/plugins/markdown-report/Report_markdown.mli
+++ b/src/plugins/markdown-report/Report_markdown.mli
@@ -1,3 +1,24 @@
+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
diff --git a/src/plugins/markdown-report/md_gen.ml b/src/plugins/markdown-report/md_gen.ml
index f8a9ba52de6d88f2106ee454f813a8968159afd4..a14c197e06bc15f4718a0cf45ec9b8e449ad3e27 100644
--- a/src/plugins/markdown-report/md_gen.ml
+++ b/src/plugins/markdown-report/md_gen.ml
@@ -1,61 +1,4 @@
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
diff --git a/src/plugins/markdown-report/md_gen.mli b/src/plugins/markdown-report/md_gen.mli
index 2e5bd59892e21acccde23b13c695ea7e6a3b22d5..69af5c51b0fb4c50daf29583b8623cf4f2ca3ea5 100644
--- a/src/plugins/markdown-report/md_gen.mli
+++ b/src/plugins/markdown-report/md_gen.mli
@@ -1,13 +1,2 @@
-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
diff --git a/src/plugins/markdown-report/mdr_params.ml b/src/plugins/markdown-report/mdr_params.ml
new file mode 100644
index 0000000000000000000000000000000000000000..d85dfc394d753ce664baa523648523d3a2890d81
--- /dev/null
+++ b/src/plugins/markdown-report/mdr_params.ml
@@ -0,0 +1,54 @@
+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)
diff --git a/src/plugins/markdown-report/mdr_params.mli b/src/plugins/markdown-report/mdr_params.mli
new file mode 100644
index 0000000000000000000000000000000000000000..1809a56e844934e8002024377331e11322b10ccb
--- /dev/null
+++ b/src/plugins/markdown-report/mdr_params.mli
@@ -0,0 +1,19 @@
+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
diff --git a/src/plugins/markdown-report/parse_remarks.ml b/src/plugins/markdown-report/parse_remarks.ml
new file mode 100644
index 0000000000000000000000000000000000000000..3e5780cf4c130b906caa8670f214ba3d3f09117b
--- /dev/null
+++ b/src/plugins/markdown-report/parse_remarks.ml
@@ -0,0 +1,78 @@
+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
diff --git a/src/plugins/markdown-report/parse_remarks.mli b/src/plugins/markdown-report/parse_remarks.mli
new file mode 100644
index 0000000000000000000000000000000000000000..d09e299ebfc4e3f53fffdddb534c8f0d15ce5467
--- /dev/null
+++ b/src/plugins/markdown-report/parse_remarks.mli
@@ -0,0 +1,6 @@
+(** 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