diff --git a/configure.in b/configure.in
index 54f3e157cd2d36381976271133d8258f25da720b..3dc68d9e3a5bc1445670594a9e111fe5f2eb779f 100644
--- a/configure.in
+++ b/configure.in
@@ -850,7 +850,7 @@ AC_ARG_ENABLE(external,
])
AC_FOREACH([__plugin],m4_esyscmd([ls src/plugins]),
- [ m4_if(m4_index(KNOWN_SRC_DIRS,__plugin),[-1],
+ [ m4_if(m4_regexp(KNOWN_SRC_DIRS,`\<__plugin\>'),[-1],
[
m4_define([plugin_dir],[src/plugins/__plugin])
m4_syscmd(test -r plugin_dir/configure.in)
diff --git a/headers/headache_config.txt b/headers/headache_config.txt
index 9bb003875b043426b796ecc87f2378b392f3f60d..17a5e0df7c761c8b616ded712cf0a62bca2d9de8 100644
--- a/headers/headache_config.txt
+++ b/headers/headache_config.txt
@@ -102,6 +102,11 @@
########
| ".*\.htm.*" -> frame open: "<!--" line: "-" close: "-->"
+########
+# XML #
+########
+| ".*\.xml" -> frame open: "<!--" line: "-" close: "-->"
+
#######
# DTD #
#######
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 3a00fb89591cebef116a40d4612856c551d31075..7da183cfb304810c8ed640831a8265fc8c1e9c88 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -873,6 +873,20 @@ src/plugins/loop_analysis/region_analysis_stmt.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/region_analysis_stmt.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/register.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/slevel_analysis.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/markdown-report/eva_coverage.ml: CEA_LGPL
+src/plugins/markdown-report/eva_coverage.mli: CEA_LGPL
+src/plugins/markdown-report/md_gen.ml: CEA_LGPL
+src/plugins/markdown-report/md_gen.mli: CEA_LGPL
+src/plugins/markdown-report/mdr_params.ml: CEA_LGPL
+src/plugins/markdown-report/mdr_params.mli: CEA_LGPL
+src/plugins/markdown-report/mdr_register.ml: CEA_LGPL
+src/plugins/markdown-report/mdr_register.mli: CEA_LGPL
+src/plugins/markdown-report/parse_remarks.ml: CEA_LGPL
+src/plugins/markdown-report/parse_remarks.mli: CEA_LGPL
+src/plugins/markdown-report/sarif_gen.ml: CEA_LGPL
+src/plugins/markdown-report/sarif_gen.mli: CEA_LGPL
+src/plugins/markdown-report/sarif.ml: CEA_LGPL
+src/plugins/markdown-report/share/acsl.xml: CEA_LGPL
src/plugins/metrics/Metrics.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/css_html.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/metrics_acsl.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/share/Makefile.dynamic b/share/Makefile.dynamic
index 4ebe6147bc6d2b7b10b77c5c0c9e035d93765a01..39658d1a462449e8780842bee27288eaeb01cfed 100644
--- a/share/Makefile.dynamic
+++ b/share/Makefile.dynamic
@@ -105,6 +105,7 @@ PLUGIN_LIB_DIR ?= $(PLUGIN_DIR)
PLUGIN_GUI_LIB_DIR ?= $(PLUGIN_DIR)/gui
PLUGIN_INSTALL_DIR ?=$(DESTDIR)$(FRAMAC_PLUGINDIR)
+ifneq ($(PLUGIN_ENABLE),no)
######################## TESTS #################
.PHONY: $(PLUGIN_NAME)_TESTS plugins_ptests_config
@@ -167,6 +168,7 @@ $(eval $(call TESTS_template))
external_tests: $(PLUGIN_NAME)_TESTS
endif
+endif # PLUGIN_ENABLE
################################################
PLUGIN_FLAGS:=$(FLAGS) $(DEBUG) $(FRAMAC_INCLUDES)
diff --git a/src/libraries/utils/markdown.ml b/src/libraries/utils/markdown.ml
index 0295d8007b6588eac586be4811bc619ef65947d2..2d00ab2478c0c64ecef50ab213d88865edd1708a 100644
--- a/src/libraries/utils/markdown.ml
+++ b/src/libraries/utils/markdown.ml
@@ -20,119 +20,142 @@
(* *)
(**************************************************************************)
-(* -------------------------------------------------------------------------- *)
-(* --- Markdown Documentation Generation Utility --- *)
-(* -------------------------------------------------------------------------- *)
-
-type md = Format.formatter -> unit
-type text = md
-type block = md
-type section = md
-
-let pretty fmt w = w fmt
-let pp_text = pretty
-let pp_block = pretty
-let pp_section = pretty
-
-(* -------------------------------------------------------------------------- *)
-(* --- Context --- *)
-(* -------------------------------------------------------------------------- *)
-
-type toc = level:int -> name:string -> title:string -> unit
-
-type context = {
- page: string ;
- path: string list ;
- names: bool ;
- level: int ;
- toc: toc option ;
+type align = Left | Center | Right
+
+type href =
+ | URL of string
+ | Page of string
+ | Section of string * string
+
+type inline =
+ | Plain of string
+ | Emph of string
+ | Bold of string
+ | Inline_code of string
+ | Link of text * href (** [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 table = {
+ caption: text option;
+ header: (text * align) list;
+ content: text list list;
}
-let context = ref {
- page = "" ;
- path = [] ;
- names = false ;
- level = 0 ;
- toc = None ;
+and element =
+ | Comment of string (** markdown comment, printed <!-- like this --> *)
+ | Block of block
+ | Table of table
+ | Raw of string list
+ (** Each element of the list is printed as-is on its own line.
+ A blank line separates the [Raw] node from the next one. *)
+ | H1 of text * string option
+ | 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
+
+and elements = element list
+
+type pandoc_markdown =
+ { title: text;
+ authors: text list;
+ date: text;
+ elements: elements
}
-let local ctxt job data =
- let current = !context in
- try context := ctxt ; job data ; context := current
- with err -> context := current ; raise err
-
-(* -------------------------------------------------------------------------- *)
-(* --- Combinators --- *)
-(* -------------------------------------------------------------------------- *)
-
-let nil _fmt = ()
-let empty= nil
-let space fmt = Format.pp_print_space fmt ()
-let newline fmt = Format.pp_print_newline fmt ()
-
-let merge sep ds fmt =
- match List.filter (fun d -> d != nil) ds with
- | [] -> ()
- | d::ds -> d fmt ; List.iter (fun d -> sep fmt ; d fmt) ds
-
-let glue ?sep ds fmt =
- match sep with
- | None -> List.iter (fun d -> d fmt) ds
- | Some s -> merge s ds fmt
-
-let (<@>) a b =
- if a == empty then b else
- if b == empty then a else
- fun fmt -> a fmt ; b fmt
-
-let (<+>) a b =
- if a == empty then b else
- if b == empty then a else
- fun fmt -> a fmt ; space fmt ; b fmt
-
-let (</>) a b =
- if a == empty then b else
- if b == empty then a else
- fun fmt -> a fmt ; newline fmt ; b fmt
-
-let fmt_text k fmt = Format.fprintf fmt "@[<h 0>%t@]" k
-let fmt_block k fmt = Format.fprintf fmt "@[<v 0>%t@]@\n" k
+let glue ?sep ls =
+ match sep , ls with
+ | (None | Some []) , _ -> List.concat ls
+ | _ , [] -> []
+ | _ , [l] -> l
+ | Some s , ls -> (* tailrec *)
+ let rec aux sep w = function
+ | [] -> List.rev w
+ | [e] -> List.rev_append w e
+ | e::el -> aux sep (List.rev_append sep (List.rev_append e w)) el
+ in aux s [] ls
(* -------------------------------------------------------------------------- *)
-(* --- Elementary Text --- *)
+(* --- Formatting --- *)
(* -------------------------------------------------------------------------- *)
-let raw s fmt = Format.pp_print_string fmt s
-let rm s fmt = Format.pp_print_string fmt s
-let it s fmt = Format.fprintf fmt "_%s_" s
-let bf s fmt = Format.fprintf fmt "**%s**" s
-let tt s fmt = Format.fprintf fmt "`%s`" s
-let text = merge space
-let praw s = fmt_block (raw s)
+let plain s = [ Plain s ]
+let emph s = [ Emph s ]
+let bold s = [ Bold s ]
+let code s = [ Inline_code s ]
+
+let format txt = Format.kasprintf plain txt
+
+let image ~alt ~file = [Image(alt,file)]
+
+let href ?text href =
+ let txt =
+ match text with Some txt -> txt | None ->
+ let tt = match href with URL u -> u | Page p -> p | Section(_,s) -> s in
+ [Inline_code tt]
+ in [Link(txt, href)]
+
+let url ?text addr = href ?text (URL addr)
+
+let link ?text ?page ?name () =
+ href ?text @@ match page, name with
+ | None, None -> Page ""
+ | Some p, None -> Page p
+ | None, Some a -> Section("",a)
+ | Some p, Some a -> Section(p,a)
+
+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]
+let enum items = [OL items]
+let description items = [DL items]
+
+let par text = [Block [Text text]]
+let block b = [Block b]
(* -------------------------------------------------------------------------- *)
-(* --- Links --- *)
+(* --- Sectioning --- *)
(* -------------------------------------------------------------------------- *)
-type href = [
- | `URL of string
- | `Page of string
- | `Name of string
- | `Section of string * string
-]
-
-let filepath m = String.split_on_char '/' m
-
-let rec relative source target =
- match source , target with
- | p::ps , q::qs when p = q -> relative ps qs
- | [] , _ -> target
- | _::d , _ -> List.map (fun _ -> "..") d @ target
-
-let lnk target =
- String.concat "/" (relative !context.path (filepath target))
-
-let id m =
+let rawfile filename =
+ let chan = open_in filename in
+ let res = ref [] in
+ try
+ while true do
+ res := input_line chan :: !res;
+ done;
+ assert false
+ with End_of_file ->
+ close_in chan;
+ [Raw (List.rev !res)]
+
+let label m =
let buffer = Buffer.create (String.length m) in
let lowercase = Char.lowercase_ascii in
let dash = ref false in
@@ -149,185 +172,279 @@ let id m =
| _ -> ()) m ;
Buffer.contents buffer
-let href ?title (h : href) fmt =
- match title , h with
- | None , `URL url -> Format.fprintf fmt "%s" url
- | Some w , `URL url -> Format.fprintf fmt "[%s](%s)" w url
- | None , `Page p -> Format.fprintf fmt "[%s](%s)" p (lnk p)
- | Some w , `Page p -> Format.fprintf fmt "[%s](%s)" w (lnk p)
- | None , `Section(p,s) -> Format.fprintf fmt "[%s](%s#%s)" s (lnk p) (id s)
- | Some w , `Section(p,s) -> Format.fprintf fmt "[%s](%s#%s)" w (lnk p) (id s)
- | None , `Name a -> Format.fprintf fmt "[%s](#%s)" a (id a)
- | Some w , `Name a -> Format.fprintf fmt "[%s](#%s)" w (id a)
+let section ?name ~title elements =
+ let anchor = label @@ match name with Some n -> n | None -> title in
+ (H1 ([Plain title], Some anchor)) :: elements
+
+let subsections header body =
+ let body =
+ List.map
+ (function
+ | H1(t,h) -> H2(t,h)
+ | H2(t,h) -> H3(t,h)
+ | H3(t,h) -> H4(t,h)
+ | H4(t,h) -> H5(t,h)
+ | e -> e)
+ (List.concat body)
+ in
+ header @ body
+
+let mk_date = function
+ | Some d -> d
+ | None ->
+ let tm = Unix.gmtime (Unix.time()) in
+ format "%d-%02d-%02d"
+ (1900 + tm.Unix.tm_year)
+ (1 + tm.Unix.tm_mon) tm.Unix.tm_mday
+
+let pandoc ?(title=[Plain ""]) ?(authors=[]) ?date elements =
+ { title; authors; date = mk_date date ; elements }
(* -------------------------------------------------------------------------- *)
-(* --- Blocks --- *)
+(* --- Printers --- *)
(* -------------------------------------------------------------------------- *)
-let aname anchor fmt =
- Format.fprintf fmt "<a name=\"%s\"></a>@\n" (id anchor)
-
-let title h ?name title fmt =
+let relativize page target =
+ let page_dir = String.split_on_char '/' page in
+ let target_dir = String.split_on_char '/' target in
+ let go_up l = List.map (fun _ -> "..") l in
+ let rec remove_common l1 l2 =
+ match l1 with
+ | [] -> assert false (* split on char is always non-empty *)
+ | [_f1] -> l2
+ | d1 :: p1 ->
+ match l2 with
+ | [] -> assert false
+ | [_f2 ] ->
+ (* it's the length of the argument to go_up that matters, not
+ its exact content *)
+ go_up p1 @ l2
+ | d2 :: p2 when d2 = d1 -> remove_common p1 p2
+ | _ -> go_up p1 @ l2
+ in
+ let relative = remove_common page_dir target_dir in
+ String.concat "/" relative
+
+let pp_href ?(page="") fmt = function
+ | URL s -> Format.pp_print_string fmt s
+ | Page s -> Format.pp_print_string fmt (relativize page s)
+ | Section (p,s) -> Format.fprintf fmt "%s#%s" (relativize page p) (label s)
+
+let rec pp_inline ?page 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](%a)@]@ "
+ (pp_text ?page) text (pp_href ?page) url
+ | Image (alt,url) -> Format.fprintf fmt "@[<h>@]@ " alt url
+
+and pp_text ?page fmt l =
+ match l with
+ | [] -> ()
+ | [ elt ] -> pp_inline ?page fmt elt
+ | elt :: text ->
+ (* tailrec *)
+ pp_inline ?page fmt elt ;
+ Format.pp_print_space fmt () ;
+ pp_text ?page fmt text
+
+let pp_lab fmt = function
+ | None -> ()
+ | Some lab -> Format.fprintf fmt " {#%s}" lab
+
+let test_size ?page txt =
+ let pp_text fmt = pp_text ?page fmt in
+ 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 ?page fmt (t,_) size =
+ let real_size = test_size ?page t in
+ let spaces = String.make (size - real_size) ' ' in
+ Format.fprintf fmt " %a%s |" (pp_text ?page) t spaces
+
+let pp_headers ?page fmt l sizes =
+ Format.fprintf fmt "@[<h>|";
+ List.iter2 (pp_header ?page fmt) l sizes;
+ Format.fprintf fmt "@]@\n"
+
+let compute_sizes headers contents =
+ let check_line i m line =
+ try max m (test_size (List.nth line i) + 2)
+ with Failure _ -> 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 ?page 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 ?page) t spaces
+
+let pp_table_line ?page fmt sizes l =
+ Format.fprintf fmt "@[<h>|";
+ List.iter2 (pp_table_cell ?page fmt) sizes l;
+ Format.fprintf fmt "@]@\n";
+ pp_sep_line fmt sizes
+
+let pp_table_content ?page fmt l sizes =
+ Format.fprintf fmt "@[<v>";
+ List.iter (pp_table_line ?page fmt sizes) l;
+ Format.fprintf fmt "@]"
+
+let pp_table_caption ?page fmt = function None -> () | Some t ->
+ Format.fprintf fmt "@[<h>Table: %a@]@\n@\n" (pp_text ?page) t
+
+[@@@ warning "-32"]
+let pp_table_extended ?page fmt { caption; header; content } =
begin
- let { level ; names ; toc } = !context in
- let level = max 0 (min 5 (level + h - 1)) in
- Format.fprintf fmt "%s %s" (String.make level '#') title ;
- if names || name <> None || toc <> None then
- begin
- let anchor = match name with None -> title | Some a -> a in
- Format.fprintf fmt " {#%s}" (id anchor) ;
- (match toc with
- | None -> ()
- | Some callback ->
- callback ~level ~name:anchor ~title) ;
- end ;
- Format.pp_print_newline fmt () ;
+ pp_table_caption ?page fmt caption;
+ let sizes = compute_sizes header content in
+ pp_sep_line fmt sizes;
+ pp_headers ?page fmt header sizes;
+ pp_aligns fmt header sizes;
+ pp_table_content ?page fmt content sizes;
end
+[@@@ warning "+32"]
-let h1 = title 1
-let h2 = title 2
-let h3 = title 3
-let h4 = title 4
-
-let indent h w fmt = local { !context with level = !context.level + h } w fmt
-
-let in_h1 = indent 1
-let in_h2 = indent 2
-let in_h3 = indent 3
-let in_h4 = indent 4
-
-let hrule fmt = Format.pp_print_string fmt "-------------------------@."
-
-let par w fmt = Format.fprintf fmt "@[<hov 0>%t@]@." w
-
-let list ws fmt =
- List.iter
- (fun w -> Format.fprintf fmt "@[<hov 2>- %t@]@." w) ws
-
-let enum ws fmt =
- let k = ref 0 in
- List.iter
- (fun w -> incr k ; Format.fprintf fmt "@[<hov 3>%d. %t@]@." !k w) ws
-
-let description items fmt =
- List.iter
- (fun (a,w) -> Format.fprintf fmt "@[<hov 2>- **%s** %t@]@." a w) items
-
-let code ?(lang="") pp fmt =
+let pp_table_inlined ?page fmt { caption; header; content } =
begin
- Format.fprintf fmt "@[<v 0>```%s" lang ;
- let buffer = Buffer.create 80 in
- let bfmt = Format.formatter_of_buffer buffer in
- pp bfmt ; Format.pp_print_flush bfmt () ;
- let content = Buffer.contents buffer in
- let lines = String.split_on_char '\n' content in
- let rec clean = function [] -> [] | ""::w -> clean w | w -> w in
+ pp_table_caption ?page fmt caption;
+ let pp = pp_text ?page in
+ Format.fprintf fmt "@[<v>@[<h>";
List.iter
- (fun l -> Format.fprintf fmt "@\n%s" l)
- (List.rev (clean (List.rev (clean lines)))) ;
- Format.fprintf fmt "@\n```@]@."
- end
-
-type column = [
- | `Left of string
- | `Right of string
- | `Center of string
-]
-
-let table columns rows fmt =
- begin
- Format.fprintf fmt "@[<v 0>" ;
+ (function (h,_) -> Format.fprintf fmt "| %a " pp h)
+ header;
+ Format.fprintf fmt "|@]@\n@[<h>";
List.iter
- (function `Left h | `Right h | `Center h -> Format.fprintf fmt "| %s " h)
- columns ;
- Format.fprintf fmt "|@\n" ;
- List.iter (fun column ->
- let dash h k = String.make (max 3 (String.length h + k)) '-' in
- match column with
- | `Left h -> Format.fprintf fmt "|:%s" (dash h 1)
- | `Right h -> Format.fprintf fmt "|%s:" (dash h 1)
- | `Center h -> Format.fprintf fmt "|:%s:" (dash h 0)
- ) columns ;
- Format.fprintf fmt "|@\n" ;
+ (fun (h,align) ->
+ let dash h k = String.make (max 3 (test_size ?page h + k)) '-' in
+ match align with
+ | Left -> Format.fprintf fmt "|:%s" (dash h 1)
+ | Right -> Format.fprintf fmt "|%s:" (dash h 1)
+ | Center -> Format.fprintf fmt "|:%s:" (dash h 0)
+ ) header;
+ Format.fprintf fmt "|@]@\n" ;
List.iter (fun row ->
- List.iter (fun col -> Format.fprintf fmt "| @[<h 0>%t@] " col) row ;
- Format.fprintf fmt "|@\n" ;
- ) rows ;
- Format.fprintf fmt "@]@." ;
+ Format.fprintf fmt "@[<h>" ;
+ List.iter
+ (fun col -> Format.fprintf fmt "| %a " pp col) row ;
+ Format.fprintf fmt "|@]@\n" ;
+ ) content ;
+ Format.fprintf fmt "@]" ;
end
-let concat ps = merge newline (List.filter (fun p -> p != empty) ps)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Refs --- *)
-(* -------------------------------------------------------------------------- *)
-
-let mk f fmt = (f ()) fmt
-let mk_text = mk
-let mk_block = mk
-
-(* -------------------------------------------------------------------------- *)
-(* --- Sections --- *)
-(* -------------------------------------------------------------------------- *)
-
-let document s = s
-
-let subsections section subsections = section </> in_h1 (merge newline subsections)
-
-let section ?name ~title content subsections =
- h1 ?name title </> content </> in_h1 (merge newline subsections)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Include File --- *)
-(* -------------------------------------------------------------------------- *)
-
-let from_file path fmt =
- let inc = open_in path in
- try
- while true do
- let line = input_line inc in
- Format.pp_print_string fmt line ;
- Format.pp_print_newline fmt () ;
- done
- with
- | End_of_file -> close_in inc
- | exn -> close_in inc ; raise exn
-
-let read_block = from_file
-let read_section = from_file
-let read_text path fmt = Format.fprintf fmt "@[<h 0>%t@]" (from_file path)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Dump to File --- *)
-(* -------------------------------------------------------------------------- *)
-
-let rec mkdir root page =
- let dir = Filename.dirname page in
- if dir <> "." && dir <> ".." then
- let path = Printf.sprintf "%s/%s" root dir in
- if not (Sys.file_exists path) then
- begin
- mkdir root dir ;
- try Unix.mkdir path 0o755
- with Unix.Unix_error _ ->
- failwith (Printf.sprintf "Can not create direcoty '%s'" dir)
- end
-
-let dump ~root ~page ?(names=false) ?toc doc =
- local
- { page ; path = filepath page ; level = 1 ; toc ; names = names }
- begin fun () ->
- mkdir root page ;
- let out = open_out (Printf.sprintf "%s/%s" root page) in
- let fmt = Format.formatter_of_out_channel out in
- try
- doc fmt ;
- Format.pp_print_newline fmt () ;
- close_out out ;
- with err ->
- Format.pp_print_newline fmt () ;
- close_out out ;
- raise err
- end ()
+let rec pp_block_element ?page fmt e =
+ let pp_text fmt = pp_text ?page fmt in
+ match e with
+ | Text t -> Format.fprintf fmt "@[<hov>%a@]@\n" pp_text t
+ | Block_quote l -> pp_quote ?page fmt l
+ | UL l -> pp_list "*" ?page fmt l
+ | OL l -> pp_list "#." ?page 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 ?page prefix fmt l =
+ List.iter
+ (fun item ->
+ Format.fprintf fmt "@[<v 4>@[<hov>%s %a@]@]"
+ prefix (pp_block ?page) item)
+ l
+
+and pp_block ?page fmt l =
+ match l with
+ | [ elt ] -> pp_block_element ?page fmt elt
+ | _ ->
+ Format.fprintf fmt "%a@\n"
+ (Format.pp_print_list
+ ~pp_sep:Format.pp_force_newline (pp_block_element ?page)) l
+
+and pp_quote ?page fmt l =
+ List.iter
+ (fun elt -> Format.fprintf fmt "@[<v>> %a@]" (pp_element ?page) elt) l
+
+and pp_element ?page fmt e =
+ let pp_text fmt = pp_text ?page fmt in
+ match e with
+ | Block b -> Format.fprintf fmt "@[<v>%a@]" (pp_block ?page) b
+ | Raw l ->
+ Format.(
+ fprintf fmt "%a"
+ (pp_print_list ~pp_sep:pp_force_newline pp_print_string) l)
+ | Comment s ->
+ Format.fprintf fmt
+ "@[<hv>@[<hov 5><!-- %a@]@ -->@]" Format.pp_print_text s
+ | Table table -> pp_table_inlined ?page fmt table
+ (* pp_table_extended ?page fmt table *)
+ | H1(t,lab) -> Format.fprintf fmt "@[<h># %a%a@]" pp_text t pp_lab lab
+ | H2(t,lab) -> Format.fprintf fmt "@[<h>## %a%a@]" pp_text t pp_lab lab
+ | H3(t,lab) -> Format.fprintf fmt "@[<h>### %a%a@]" pp_text t pp_lab lab
+ | H4(t,lab) -> Format.fprintf fmt "@[<h>#### %a%a@]" pp_text t pp_lab lab
+ | H5(t,lab) -> Format.fprintf fmt "@[<h>##### %a%a@]" pp_text t pp_lab lab
+ | H6(t,lab) -> Format.fprintf fmt "@[<h>###### %a%a@]" pp_text t pp_lab lab
+
+and pp_elements ?page fmt l =
+ let pp_sep fmt () =
+ Format.pp_print_newline fmt ();
+ Format.pp_print_newline fmt ()
+ in
+ Format.pp_print_list ~pp_sep (pp_element ?page) fmt l
+
+let pp_authors ?page fmt l =
+ List.iter (fun t -> Format.fprintf fmt "@[<h>- %a@]@\n" (pp_text ?page) t) l
+
+let pp_pandoc ?page 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 ?page) title;
+ Format.fprintf fmt "@[<h>author:@]@\n%a" (pp_authors ?page) authors;
+ Format.fprintf fmt "@[<h>date: %a@]@\n" (pp_text ?page) date;
+ Format.fprintf fmt "@[<h>...@]@\n";
+ Format.pp_print_newline fmt ();
+ end;
+ pp_elements ?page fmt elements;
+ Format.fprintf fmt "@]%!"
(* -------------------------------------------------------------------------- *)
diff --git a/src/libraries/utils/markdown.mli b/src/libraries/utils/markdown.mli
index 34b955919fcc8696722172e66ad43680b689335c..79f35f876fbe3662e366dede54295bfcbd883bf3 100644
--- a/src/libraries/utils/markdown.mli
+++ b/src/libraries/utils/markdown.mli
@@ -20,164 +20,204 @@
(* *)
(**************************************************************************)
-(* -------------------------------------------------------------------------- *)
-(* --- Markdown Documentation Generation Utility --- *)
-(* -------------------------------------------------------------------------- *)
-
-(** {2 Markdown}
-
- A lightweight helper for generating Markdown documentation.
- Two levels of formatters are defined to help managing indentation and
- spaces: [text] for inline markdown, and [block] for markdown paragraphs.
-
+(** {2 Markdown Document}
+ Structured representation of Markdown content. *)
+
+(** Table columns alignment *)
+type align = Left | Center | Right
+
+(** Local refs and URLs *)
+type href =
+ | URL of string
+ (** URL href is printed as it is. *)
+
+ | Page of string
+ (** URL relative to a common root.
+ During pretty-printing, if given the path of the current
+ document, the string will be modified accordingly. For instance,
+ when writing to [foo/bar.md], [Page "foo/bla.md"] will be output as
+ [(bla.md)].
+ *)
+
+ | Section of string * string
+ (** URL of an anchor within a [Page], see above. *)
+
+type inline =
+ | Plain of string (** Printed as it is *)
+ | Emph of string (** Printed as ["_……_"] *)
+ | Bold of string (** Printed as ["**……**"] *)
+ | Inline_code of string (** Printed as ["`……`"] *)
+ | Link of text * href (** Hyperlink with text and URL *)
+ | Image of string * string (** [Image(alt,path)] with alternative text and image file *)
+
+and text = inline list (** Inline elements separated by spaces *)
+
+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 table = {
+ caption: text option;
+ header: (text * align) list;
+ content: text list list;
+}
+
+and element =
+ | Comment of string (** markdown comment, printed <!-- like this --> *)
+ | Block of block
+ | Table of table
+ | Raw of string list
+ (** Each element of the list is printed as-is on its own line.
+ A blank line separates the [Raw] node from the next one. *)
+ | H1 of text * string option
+ | 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
+
+and elements = element list
+
+type pandoc_markdown =
+ { title: text;
+ authors: text list;
+ date: text;
+ elements: elements
+ }
+
+(** {2 Formatting Utilities}
+
+ Remark: [text] values are list of [inline] values, hence
+ you may combined with the [(@)] operator or with the [glue ?sep] utility
+ function (see below).
*)
-type text
-type block
-type section
-
-val (<@>) : text -> text -> text (** Infix operator for [glue] *)
-val (<+>) : text -> text -> text (** Infix operator for [text] *)
-val (</>) : block -> block -> block (** Infix operator for [concat] *)
+(** Plain markdown *)
+val plain: string -> text
-(** {2 Text Constructors} *)
+(** Emph text *)
+val emph: string -> text
-val nil : text (** Empty *)
-val raw : string -> text (** inlined markdown format *)
-val rm : string -> text (** roman (normal) style *)
-val it : string -> text (** italic style *)
-val bf : string -> text (** bold style *)
-val tt : string -> text (** typewriter style *)
+(** Bold text *)
+val bold: string -> text
-val glue : ?sep:text -> text list -> text (** Glue text fragments *)
-val text : text list -> text (** Glue text fragments with spaces *)
+(** Inline code *)
+val code: string -> text
-(** {2 Block Constructors} *)
+(** Image *)
+val image: alt:string -> file:string -> text
-val empty : block (** Empty *)
-val hrule : block (** Horizontal rule *)
+(** Href link *)
+val href: ?text:text -> href -> text
-val h1 : ?name:string -> string -> block (** Title level 1 *)
-val h2 : ?name:string -> string -> block (** Title level 2 *)
-val h3 : ?name:string -> string -> block (** Title level 3 *)
-val h4 : ?name:string -> string -> block (** Title level 4 *)
+(** Local links *)
+val link: ?text:text -> ?page:string -> ?name:string -> unit -> text
-val in_h1 : block -> block (** Increment title levels by 1 *)
-val in_h2 : block -> block (** Increment title levels by 2 *)
-val in_h3 : block -> block (** Increment title levels by 3 *)
-val in_h4 : block -> block (** Increment title levels by 4 *)
+(** URL links *)
+val url: ?text:text -> string -> text
-val par : text -> block (** Simple text paragraph *)
-val praw : string -> block (** Simple raw paragraph *)
-val list : text list -> block (** Itemized list *)
-val enum : text list -> block (** Enumerated list *)
-val description : (string * text) list -> block (** Description list *)
+(** Plain markdown content of the formatted string *)
+val format: ('a, Format.formatter, unit, text) format4 -> 'a
-(** Formatted code.
+(** {2 Blocks Utilities}
- The code content is pretty-printed in a vertical [<v0>] box
- with default [Format] formatter.
- Leading and trailing empty lines are removed and indentation is
- preserved. *)
-val code : ?lang:string -> (Format.formatter -> unit) -> block
+ Remark: [block] values are list of [block_element] values, hence
+ you may combined with the [(@)] operator or with the [glue ?sep] utility
+ function (see below).
+*)
-val concat : block list -> block (** Glue paragraphs with empty lines *)
+(** Text Block *)
+val text : text -> block
-(** {2 Hyperlinks}
+(** Itemized list *)
+val list : block list -> block
- [`Page], [`Name] and [`Section] links refers to the current document,
- see [dump] function below.
+(** Enumerated list *)
+val enum : block list -> block
- In [`Section(p,t)], [p] is the page path relative to the
- document {i root}, and [t] is the section title {i or} name.
+(** Description list *)
+val description : (text * text) list -> block
- For [`Name a], the links refers to name or title [a]
- in the {i current} page.
+(** [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
- Hence, everywhere throughout a self-content document directory [~root],
- local page [~page] inside [~root] can be referenced
- by [`Page page], and its sections can by [`Section(page,title)]
- or [`Section(page,name)].
+(** {2 Document Elements}
+ Remark: [elements] values are list of [element] values, hence
+ you may combined with the [(@)] operator or with the [glue ?sep] utility
+ function (see below).
*)
-type href = [
- | `URL of string
- | `Page of string
- | `Name of string
- | `Section of string * string
-]
-
-(** Default [~title] is taken from [href]. When printed,
- actual link will be relativized with respect to current page. *)
-val href : ?title:string -> href -> text
-
-(** Define a local anchor *)
-val aname : string -> block
+(** Single Paragraph element *)
+val par : text -> elements
-(** {2 Tables} *)
+(** Block element *)
+val block : block -> elements
-type column = [
- | `Left of string
- | `Right of string
- | `Center of string
-]
-
-val table : column list -> text list list -> block
+(** Get the content of a file as raw markdown.
+ @raise Sys_error if there's no such file.
+*)
+val rawfile: string -> elements
-(** {2 Markdown Generator}
- Generating function are called each time the markdown
- fragment is printed. *)
+(** {2 Document Structure} *)
-val mk_text : (unit -> text) -> text
-val mk_block : (unit -> block) -> block
+(** Creates a document from a list of elements and optional metadatas.
+ Defaults are:
+ - title: empty
+ - authors: empty list
+ - date: current day, in ISO format
+*)
+val pandoc:
+ ?title:text -> ?authors: text list -> ?date: text -> elements ->
+ pandoc_markdown
-(** {2 Sections}
+(** Adds a [H1] header with the given [title] on top of the given elements.
+ If name is not explicitly provided,
+ the header will have as associated anchor [id title]
+*)
+val section: ?name:string -> title:string -> elements -> elements
- Sections are an alternative to [h1-h4] constructors to build
- properly nested sub-sections. Deep sections at depth 5 and more are
- flattened.
+(** [subsections header body] returns a list of [element]s where the [body]'s
+ headers have been increased by one (i.e. [H1] becomes [H2]).
+ [H5] stays at [H5], though.
*)
+val subsections: elements -> elements list -> elements
-val section : ?name:string -> title:string -> block -> section list -> section
-val subsections : section -> section list -> section
-val document : section -> block
+(** {2 Other Utilities} *)
-(** {2 Dump to file}
+(** Glue fragments, typically used for combining [text], [block]
+ and [elements].
+ Default separator is empty. The function is tail-recursive. *)
+val glue: ?sep:'a list -> 'a list list -> 'a list
- Generate the markdown [~page] in directory [~root] with the given content.
- The [~root] directory shall be absolute or relative to the current working
- directory. The [~page] file-path shall be relative to the [~root] directory
- and will be used to relocate hyperlinks to other [`Page] and [`Section]
- properly.
+(** Transforms a string into an anchor name, roughly following
+ pandoc's conventions. This function is automatically used
+ by pretty-printers and smart constructors to normalize section names
+ and local links. *)
+val label: string -> string
- Hence, everywhere throughout the document, [dump ~root ~page doc]
- is referenced by [`Page page], and its sections are referenced by
- [`Section(page,title)].
+(** {2 Pretty-printers} *)
-*)
+val pp_inline: ?page:string -> Format.formatter -> inline -> unit
-(** Callback to listen for actual sections when printing a page. *)
-type toc = level:int -> name:string -> title:string -> unit
+val pp_text: ?page:string -> Format.formatter -> text -> unit
-(** Create a markdown page.
- - [~root] document directory (relocatable)
- - [~page] relative file-path of the page in [~root] (non relocatable)
- - [~names] generate explicit [<a name=...>] tags for all titles
- - [~toc] optional callback to register table of contents
-*)
-val dump : root:string -> page:string -> ?names:bool -> ?toc:toc -> block -> unit
+val pp_block_element: ?page:string -> Format.formatter -> block_element -> unit
-(** {2 Miscellaneous} *)
+val pp_block: ?page:string -> Format.formatter -> block -> unit
-val read_text : string -> text
-val read_block : string -> block
-val read_section : string -> section
+val pp_element: ?page:string -> Format.formatter -> element -> unit
-val fmt_text : (Format.formatter -> unit) -> text
-val fmt_block : (Format.formatter -> unit) -> block
-val pp_text : Format.formatter -> text -> unit
-val pp_block : Format.formatter -> block -> unit
-val pp_section : Format.formatter -> section -> unit
+val pp_elements: ?page:string -> Format.formatter -> elements -> unit
-(* -------------------------------------------------------------------------- *)
+val pp_pandoc: ?page:string -> Format.formatter -> pandoc_markdown -> unit
diff --git a/src/plugins/markdown-report/.gitignore b/src/plugins/markdown-report/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..6c2faaa71d31861e38605eb6bebc51dec9a0e3da
--- /dev/null
+++ b/src/plugins/markdown-report/.gitignore
@@ -0,0 +1,14 @@
+*.cm*
+META.*
+*.o
+top/
+*.check_mli_exists
+.Makefile.plugin.generated
+.depend
+.merlin
+*~
+/Makefile
+/Markdown_report.mli
+/tests/ptests_config
+/tests/*/result
+/tests/*/result_*
diff --git a/src/plugins/markdown-report/LICENSE b/src/plugins/markdown-report/LICENSE
new file mode 100644
index 0000000000000000000000000000000000000000..d0aa4f37090a964609695d3d8155e9999abb9a21
--- /dev/null
+++ b/src/plugins/markdown-report/LICENSE
@@ -0,0 +1,9 @@
+Files in this directory are part of the MarkDown Report Frama-C plug-in.
+
+Copyright (C) 2007-2018
+ CEA (Commissariat à l'énergie atomique et aux énergies
+ alternatives)
+
+All rights reserved.
+Contact CEA LIST for licensing.
+
diff --git a/src/plugins/markdown-report/Makefile.in b/src/plugins/markdown-report/Makefile.in
new file mode 100644
index 0000000000000000000000000000000000000000..9ef075fbc3af4e828df07e21331769878dc4119f
--- /dev/null
+++ b/src/plugins/markdown-report/Makefile.in
@@ -0,0 +1,34 @@
+ifndef FRAMAC_SHARE
+ FRAMAC_SHARE:=$(shell frama-c -print-share-path)
+endif
+
+PLUGIN_NAME:=Markdown_report
+PLUGIN_GENERATED:=$(PLUGIN_DIR)/Markdown_report.mli
+PLUGIN_CMO:=\
+ sarif mdr_params parse_remarks \
+ eva_coverage md_gen sarif_gen mdr_register
+PLUGIN_REQUIRES:=ppx_deriving ppx_deriving_yojson yojson
+PLUGIN_DISTRIB_EXTERNAL:=share/acsl.xml
+PLUGIN_TESTS_DIRS:= eva
+PLUGIN_ENABLE:=@ENABLE_MDR@
+
+include $(FRAMAC_SHARE)/Makefile.dynamic
+
+$(Markdown_report_DIR)/Markdown_report.mli: \
+ $(Markdown_report_DIR)/mdr_params.mli \
+ $(Markdown_report_DIR)/md_gen.mli \
+ $(Markdown_report_DIR)/Makefile
+ echo "module Mdr_params: sig" > $@
+ cat $(Markdown_report_DIR)/mdr_params.mli >> $@
+ echo "end" >> $@
+ echo "module Md_gen: sig" >> $@
+ cat $(Markdown_report_DIR)/md_gen.mli >> $@
+ echo "end" >> $@
+
+ifeq ("@ENABLE_MDR@","yes")
+install::
+ $(PRINT_CP) $(FRAMAC_DATADIR)/Markdown_report
+ $(MKDIR) $(FRAMAC_DATADIR)/Markdown_report
+ $(CP) $(Markdown_report_DIR)/share/acsl.xml \
+ $(FRAMAC_DATADIR)/Markdown_report
+endif
diff --git a/src/plugins/markdown-report/README.md b/src/plugins/markdown-report/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..86db9c1694633b271267538b55aae070ac230310
--- /dev/null
+++ b/src/plugins/markdown-report/README.md
@@ -0,0 +1,79 @@
+Generation of pandoc and/or sarif 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.
+
+# Dependencies
+
+## Mandatory
+- OCaml >= 4.04;
+- Frama-C 18.0 (Argon)
+- packages `ppx_deriving`, `ppx_deriving_yojson` and `yojson`
+
+**Important Note** In the current version of `ppx_deriving`, the `META` file
+provided misses a line indicating how to load the package in a dynamic manner
+(i.e. what Frama-C does when loading its plug-in), preventing the plug-in
+to be loaded by Frama-C. If Frama-C fails to load the plug-in, please add
+the line
+
+```
+plugin(native) = "ppx_deriving_runtime.cmxs"
+```
+
+to the `package "runtime"` record of the file
+`$(ocamlfind query ppx_deriving)/META`
+
+## Optional
+- FlameGraph ([`https://github.com/brendangregg/FlameGraph`](https://github.com/brendangregg/FlameGraph))
+
+# Installation
+
+Running `make` and `make install` (possibly with admin rights depending on
+your installation of Frama-C) should compile and install the plugin in
+Frama-C's installation directory.
+
+# Usage
+
+MarkDownReport focuses on results computed by Eva. It has three output formats,
+controlled by the `-mdr-gen` option:
+
+- `draft`: produces a markdown report with placeholders for writing (markdown)
+comments on the various items (e.g. why is an alarm spurious, or why is
+a given hypothesis safe).
+- `markdown`: produces a full-fledged markdown report. It can be used in
+ conjunction with the option `-mdr-remarks <f>` which will use the
+ remarks written in the draft document `f` (which is supposed to have been
+ generated from the same analysis in `draft` mode and edited with manual
+ comments afterwards).
+- `sarif`: produces a json object in the Static Analysis Results Interchange
+ Format (SARIF), as documented [here](https://github.com/oasis-tcs/sarif-spec).
+ This output is very experimental and lacks many information contained in
+ the `markdown` format. It can also incorporate remarks from `-mdr-remarks`,
+ that will be reflected as `message`s in the `sarif` object.
+
+The output file can be controlled with `-mdr-out`. Other options are:
+
+- `-mdr-authors`: comma separated list of the authors of the document
+- `-mdr-title`: give a title to the document
+- `-mdr-flamegraph`: generate a flamegraph in the given file (see below)
+- `-mdr-stubs`: identifies a set of files as containing stubs for Eva (i.e.
+ code that is not in the scope of the analysis per se).
+
+Sarif document can be validated against the spec
+[online](https://sarifweb.azurewebsites.net/Validation)
+
+## Flamegraph
+Checking out [`https://github.com/Frama-C/open-source-case-studies`](https://github.com/Frama-C/open-source-case-studies), start with a simple analysis and generate the intermediary SVG and Markdown files.
+
+```shell
+frama-c -val 2048.c -val-flamegraph="flamegraph.txt" -save snap.sav
+flamegraph.pl ./flamegraph.txt > flamegraph.svg
+frama-c -load snap.sav -mdr-gen -mdr-flamegraph="./flamegraph.svg"
+```
+
+Then generate a report in your favorite open format (requires the
+[pandoc](http://pandoc.org/) document generator
+
+```shell
+pandoc -o report.docx report.md
+```
diff --git a/src/plugins/markdown-report/configure.ac b/src/plugins/markdown-report/configure.ac
new file mode 100644
index 0000000000000000000000000000000000000000..e58d4f1b60c623f240184747f20699d3e3f0d972
--- /dev/null
+++ b/src/plugins/markdown-report/configure.ac
@@ -0,0 +1,24 @@
+m4_define([plugin_file],Makefile.in)
+
+m4_define([FRAMAC_SHARE_ENV],
+ [m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
+
+m4_define([FRAMAC_SHARE],
+ [m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
+ [m4_esyscmd(frama-c -print-path)])])
+
+m4_ifndef([FRAMAC_M4_MACROS],
+ [m4_include(FRAMAC_SHARE/configure.ac)]
+ )
+
+check_plugin(mdr,PLUGIN_RELATIVE_PATH(plugin_file),[Mardown/SARIF report plug-in],yes)
+
+plugin_require_pkg(mdr,ppx_deriving)
+plugin_require_pkg(mdr,ppx_deriving_yojson)
+
+configure_pkg(ppx_deriving,[package ppx_deriving not found])
+configure_pkg(ppx_deriving_yojson,[package ppx_deriving_yojson not found])
+
+check_plugin_dependencies
+
+write_plugin_config(Makefile)
diff --git a/src/plugins/markdown-report/eva_coverage.ml b/src/plugins/markdown-report/eva_coverage.ml
new file mode 100644
index 0000000000000000000000000000000000000000..d60250838fc374a5a9753c7378fa42cfa1f5c5d8
--- /dev/null
+++ b/src/plugins/markdown-report/eva_coverage.ml
@@ -0,0 +1,230 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+type coverage_stats =
+ { syntactic_calls: int;
+ indirect_calls: int;
+ total_stmts: int;
+ covered_stmts: int; }
+
+let add_syntactic_call stats =
+ { stats with syntactic_calls = stats.syntactic_calls + 1 }
+
+let add_indirect_call stats =
+ { stats with indirect_calls = stats.indirect_calls + 1 }
+
+let empty_stats =
+ { syntactic_calls = 0;
+ indirect_calls = 0;
+ total_stmts = 0;
+ covered_stmts = 0 }
+
+type call_kind = No_call | Only_indirect | Direct
+
+type callee_info = { call: call_kind;
+ is_analyzed: bool;
+ visited: bool; }
+
+let no_call =
+ { call = No_call; is_analyzed = false; visited = false; }
+
+let indirect_call = { no_call with call = Only_indirect }
+
+let direct_call = { indirect_call with call = Direct }
+
+let visit info = { info with visited = true; }
+
+let is_analyzed_function vi =
+ not (Cil.hasAttribute "fc_stdlib" vi.vattr) &&
+ not (Cil.hasAttribute "fc_stdlib_generated" vi.vattr) &&
+ Kernel_function.is_definition (Globals.Functions.get vi) &&
+ not (List.exists
+ (fun s ->
+ List.exists
+ (fun kf ->
+ Cil_datatype.Varinfo.equal
+ (Kernel_function.get_vi kf)
+ vi)
+ (Globals.FileIndex.get_functions
+ (Filepath.Normalized.of_string s)))
+ (Mdr_params.Stubs.get())) &&
+ not (List.mem vi.vname
+ (String.split_on_char ','
+ (Dynamic.Parameter.String.get "-eva-use-spec" ()))) &&
+ not (List.mem vi.vname
+ (List.map
+ (fun s -> List.hd (String.split_on_char ':' s))
+ (String.split_on_char ','
+ (Dynamic.Parameter.String.get "-eva-builtin" ()))))
+
+let is_analyzed_info vi info = {info with is_analyzed=is_analyzed_function vi; }
+
+
+class eva_coverage_vis ~from_entry_point = object(self)
+ inherit Visitor.frama_c_inplace
+ val mutable stats = empty_stats
+ val calls = Cil_datatype.Varinfo.Hashtbl.create 17
+
+ method private incr_total_stmts =
+ stats <- { stats with total_stmts = stats.total_stmts + 1 }
+ method private incr_covered_stmts =
+ stats <- { stats with covered_stmts = stats.covered_stmts + 1 }
+
+ method! vstmt_aux s =
+ (* We only consider real statements: Blocks do not count. *)
+ match s.skind with
+ | Block _ | UnspecifiedSequence _ -> Cil.DoChildren
+ | _ ->
+ self#incr_total_stmts;
+ if Db.Value.is_reachable_stmt s then self#incr_covered_stmts;
+ Cil.DoChildren
+
+ method! vinst i =
+ match i with
+ | Call(_, { enode = Lval (Var vi, NoOffset)},_,_)
+ | Local_init(_,ConsInit (vi,_,_),_) ->
+ if Cil_datatype.Varinfo.Hashtbl.mem calls vi then begin
+ let info = Cil_datatype.Varinfo.Hashtbl.find calls vi in
+ Cil_datatype.Varinfo.Hashtbl.replace
+ calls vi { info with call = Direct }
+ end else begin
+ Cil_datatype.Varinfo.Hashtbl.add
+ calls vi (is_analyzed_info vi direct_call)
+ end;
+ Cil.SkipChildren
+ | Call(_,{ enode = Lval (Mem _,NoOffset)},_,_) ->
+ let s = Extlib.the self#current_stmt in
+ let kfs = Db.Value.call_to_kernel_function s in
+ let handle_one kf =
+ let vi = Kernel_function.get_vi kf in
+ if not (Cil_datatype.Varinfo.Hashtbl.mem calls vi)
+ then begin
+ Cil_datatype.Varinfo.Hashtbl.add
+ calls vi (is_analyzed_info vi indirect_call)
+ end else begin
+ let info = Cil_datatype.Varinfo.Hashtbl.find calls vi in
+ if info.call = No_call then begin
+ Cil_datatype.Varinfo.Hashtbl.replace
+ calls vi { info with call = Only_indirect }
+ end
+ end
+ in
+ Kernel_function.Hptset.iter handle_one kfs;
+ Cil.SkipChildren
+ | _ -> Cil.SkipChildren (* No need to go further. *)
+
+ method compute () =
+ let treat_call vi info reached =
+ let must_visit = not info.visited && info.is_analyzed in
+ Cil_datatype.Varinfo.Hashtbl.replace calls vi (visit info);
+ if must_visit then begin
+ let kf = Globals.Functions.get vi in
+ ignore (Visitor.visitFramacKf (self:>Visitor.frama_c_inplace) kf);
+ end;
+ reached && not must_visit
+ in
+ let check_fixpoint () =
+ Cil_datatype.Varinfo.Hashtbl.fold treat_call calls true
+ in
+ if not from_entry_point then begin
+ Globals.Functions.iter_on_fundecs
+ (fun { svar } ->
+ Cil_datatype.Varinfo.Hashtbl.add
+ calls svar (is_analyzed_info svar no_call))
+ end;
+ let vi =
+ Globals.Functions.get_vi
+ (Globals.Functions.find_by_name (Kernel.MainFunction.get()))
+ in
+ (* main entry point might be a stub, but we still would like
+ to collect non-stubs calls from it.
+ *)
+ let info = is_analyzed_info vi direct_call in
+ Cil_datatype.Varinfo.Hashtbl.replace
+ calls vi { info with is_analyzed = true };
+ while not (check_fixpoint ()) do () done;
+ Cil_datatype.Varinfo.Hashtbl.fold
+ (fun _ info stats ->
+ if info.is_analyzed then begin
+ match info.call with
+ | Direct -> add_syntactic_call stats
+ | Only_indirect -> add_indirect_call stats
+ | No_call -> stats
+ end else stats)
+ calls
+ stats
+
+end
+
+let nb_fundefs () =
+ Globals.Functions.fold
+ (fun kf nb ->
+ if Kernel_function.is_definition kf &&
+ is_analyzed_function (Kernel_function.get_vi kf)
+ then nb + 1 else nb) 0
+
+let md_gen () =
+ let main = Kernel.MainFunction.get () in
+ !Db.Value.compute ();
+ let vis = new eva_coverage_vis ~from_entry_point:false in
+ let stats = vis#compute () in
+ let summary_whole =
+ Markdown.format
+ "There are %d function definitions that are not stubbed. They represent \
+ %d statements, of which %d are potentially reachable through EVA, \
+ resulting in a **statement coverage of %.1f%%** with respect to the \
+ entire application."
+ (nb_fundefs())
+ stats.total_stmts stats.covered_stmts
+ (float_of_int stats.covered_stmts *. 100. /.
+ float_of_int stats.total_stmts)
+ in
+ let vis = new eva_coverage_vis ~from_entry_point:true in
+ let stats = vis#compute () in
+ let summary =
+ Markdown.format
+ "There were potentially %d functions syntactically reachable from %s."
+ stats.syntactic_calls main
+ in
+ let summary =
+ if stats.indirect_calls = 0 then summary
+ else
+ summary @
+ Markdown.format
+ "In addition, %d were found potentially reachable through \
+ indirect calls."
+ stats.indirect_calls
+ in
+ let summary =
+ summary @
+ Markdown.format
+ "These functions contain %d statements, \
+ of which %d are potentially reachable according to EVA, resulting in \
+ a **statement coverage of %.1f%%** with respect to the perimeter set \
+ by this entry point."
+ stats.total_stmts stats.covered_stmts
+ (float_of_int stats.covered_stmts *. 100. /.
+ float_of_int stats.total_stmts)
+ in
+ Markdown.([ Block [Text summary_whole]; Block [Text summary ]])
diff --git a/src/plugins/markdown-report/eva_coverage.mli b/src/plugins/markdown-report/eva_coverage.mli
new file mode 100644
index 0000000000000000000000000000000000000000..b90ba900cfcbf521ee9a9d6b7003d465fdbb565f
--- /dev/null
+++ b/src/plugins/markdown-report/eva_coverage.mli
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** generates a coverage summary of EVA's run*)
+val md_gen: unit -> Markdown.element list
diff --git a/src/plugins/markdown-report/md_gen.ml b/src/plugins/markdown-report/md_gen.ml
new file mode 100644
index 0000000000000000000000000000000000000000..b87147c29958017ea76f02a5860faf62eac53c52
--- /dev/null
+++ b/src/plugins/markdown-report/md_gen.ml
@@ -0,0 +1,637 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Markdown
+
+type env =
+ { is_draft: bool;
+ remarks: Markdown.element list Datatype.String.Map.t; }
+
+let insert_remark_opt env anchor placeholder =
+ try Datatype.String.Map.find anchor env.remarks with Not_found -> placeholder
+
+let insert_remark env anchor = insert_remark_opt env anchor []
+
+(* apparently, pandoc, or at least its latex output,
+ does not like anchors beginning with _ *)
+let sanitize_anchor s =
+ if s = "" then "a"
+ else if s.[0] = '_' then "a" ^ s
+ else s
+
+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 insert_marks env anchor =
+ Comment "BEGIN_REMARK"
+ :: insert_remark env anchor
+ @ [Comment "END_REMARK"]
+
+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" @ bold x), plain y)
+ all_eva_domains
+
+let section_domains env =
+ let anchor = "domains" in
+ let head = H3 (plain "EVA Domains", Some anchor) in
+ if env.is_draft then
+ head
+ :: Comment "You can give more information about the choice of EVA domains"
+ :: insert_marks env anchor
+ else begin
+ let l = get_eva_domains () in
+ head
+ :: 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]
+ )
+ :: insert_remark env anchor
+ end
+
+let section_stubs env =
+ let stubbed_kf =
+ List.concat
+ (List.map
+ (fun f ->
+ let filename = Filepath.Normalized.of_string f in
+ Globals.FileIndex.get_functions ~declarations:false filename)
+ (Mdr_params.Stubs.get ())
+ )
+ in
+ let stubbed_kf = List.filter Kernel_function.is_definition stubbed_kf in
+ let opt = Dynamic.Parameter.String.get "-eva-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
+ let anchor = sanitize_anchor s in
+ let content =
+ if env.is_draft then insert_marks env anchor
+ else
+ let intro = Markdown.text @@ Markdown.format
+ "`%s` has the following specification" s in
+ let funspec = Markdown.codeblock ~lang:"acsl" "%a"
+ Printer.pp_funspec (Annotations.funspec kf) in
+ Block ( intro @ funspec ) :: insert_remark env anchor
+ in
+ H4 (code s, Some anchor) :: content)
+ l
+ in
+ let describe_func kf =
+ let name = Kernel_function.get_name kf in
+ let anchor = sanitize_anchor name in
+ let loc = Kernel_function.get_location kf in
+ let content =
+ if env.is_draft then insert_marks env anchor
+ else
+ let intro = Markdown.text @@ Markdown.format
+ "`%s` @[<h>is defined at %a@]"
+ name Cil_datatype.Location.pretty loc in
+ 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
+ H4 (code name, Some anchor) :: content
+ in
+ let content =
+ if stubbed_kf <> [] then begin
+ List.map describe_func stubbed_kf
+ end else []
+ in
+ let content = content @ use_spec in
+ let content = List.concat content in
+ if content = [] then
+ if env.is_draft then
+ [ Comment "No stubs have been used" ]
+ else
+ [ Block [Text (plain "No stubs have been used for this analysis")]]
+ else
+ content
+
+let get_files () =
+ let dir_table = Datatype.String.Hashtbl.create 17 in
+ let add_entry f =
+ let dir = Filename.dirname f in
+ let base = Filename.basename f in
+ let suf =
+ try
+ let i = String.rindex base '.' in
+ String.sub base i (String.length base - i)
+ with Not_found -> ""
+ in
+ let entries =
+ try Datatype.String.Hashtbl.find dir_table dir
+ with Not_found -> Datatype.String.Map.empty
+ in
+ let subentries =
+ try Datatype.String.Map.find suf entries
+ with Not_found -> Datatype.String.Set.empty
+ in
+ Datatype.String.(
+ Hashtbl.replace
+ dir_table dir (Map.add suf (Set.add base subentries) entries))
+ in
+ List.iter add_entry (Kernel.Files.get());
+ let treat_subentry dir dir_files suf files l =
+ let dir_files =
+ List.fold_left
+ (fun acc s ->
+ if Filename.check_suffix s suf then Datatype.String.Set.add s acc
+ else acc)
+ Datatype.String.Set.empty dir_files
+ in
+ if Datatype.String.Set.subset dir_files files then
+ (dir ^ "/*" ^ suf) :: l
+ else
+ Datatype.String.Set.elements files @ l
+ in
+ let treat_entry dir map l =
+ try
+ let dir_files = Array.to_list (Sys.readdir dir) in
+ Datatype.String.Map.fold (treat_subentry dir dir_files) map l
+ with Sys_error s ->
+ Mdr_params.warning "Unable to find directory %s: %s" dir s;
+ Datatype.String.Map.fold
+ (fun _ s l -> Datatype.String.Set.elements s @ l) map l
+ in
+ Datatype.String.Hashtbl.fold treat_entry dir_table []
+
+let gen_inputs env =
+ let anchor = "c-input" in
+ let prelude =
+ if env.is_draft then
+ Comment
+ "You can add here some remarks about the set of files \
+ that is considered by Frama-C"
+ :: insert_marks env anchor
+ else
+ insert_remark env anchor
+ in
+ H2 (plain "Input files", Some anchor)
+ :: prelude
+ @ [
+ 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 @@ code x) (get_files()));
+ ]]
+
+let gen_config env =
+ let anchor = "options" in
+ let header = H2 (plain "Configuration", Some anchor) in
+ let content =
+ if env.is_draft then
+ Comment
+ "You can add here some remarks about the options used for the analysis"
+ :: insert_marks env anchor
+ else begin
+ let placeholder = [
+ Block [
+ Text
+ (plain "The options that have been used for this analysis \
+ are the following.")]]
+ in insert_remark_opt env anchor placeholder
+ end
+ in
+ header :: content
+
+let gen_context env =
+ let context =
+ let anchor = "intro" in
+ let header = H1 (plain "Introduction", Some anchor) in
+ if env.is_draft then
+ header
+ :: Comment "You can add here some overall introduction to the analysis"
+ :: insert_marks env anchor
+ else begin
+ match insert_remark env anchor with
+ | [] -> []
+ | (_::_) as l -> header :: l
+ end
+ in
+ context @
+ H1 (plain "Context of the analysis", Some "context")
+ :: gen_inputs env
+ @ gen_config env
+ @ section_domains env
+ @ H3 (plain "Stubbed Functions", Some "stubs")
+ :: (
+ if env.is_draft then
+ Comment
+ "You can add here general comments about the stubs that have been used"
+ :: insert_marks env "stubs"
+ else insert_remark env "stubs")
+ @ section_stubs env
+
+let gen_coverage env =
+ let anchor = "coverage" in
+ let header = H1 (plain "Coverage", Some anchor) in
+ let content = Eva_coverage.md_gen () in
+ let content =
+ if env.is_draft then
+ content @
+ Comment "You can comment on the coverage obtained by EVA"
+ :: insert_marks env anchor
+ else
+ content @ insert_remark env anchor
+ in
+ header :: content
+
+let string_of_pos pos = Format.asprintf "%a" Filepath.pp_pos pos
+
+let string_of_pos_opt =
+ function
+ | None -> "Global"
+ | Some pos -> string_of_pos pos
+
+let string_of_loc (l1, _) = string_of_pos l1
+
+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 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 (string_of_pos_opt evt_source);
+ format "`%s` (emitted by `%s`)" evt_message evt_plugin ]
+ 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 section_event is_err env nb event =
+ let open Log in
+ let title =
+ Format.asprintf "@[<h>%s %d (%s)@]"
+ (if is_err then "Error" else "Warning")
+ nb
+ (string_of_pos_opt event.evt_source)
+ in
+ let lab =
+ Format.asprintf "@[<h>%s-%d@]" (if is_err then "err" else "warn") nb
+ in
+ let content =
+ if env.is_draft then
+ insert_marks env lab
+ else insert_remark env lab
+ in
+ H2 (plain title, Some lab)
+ :: Block (
+ (text @@ plain "Message:") @
+ codeblock "[%s] %s" event.evt_plugin event.evt_message
+ )
+ :: content
+
+let make_events_list is_err env l =
+ List.concat (List.mapi (section_event is_err env) l)
+
+let make_errors_list = make_events_list true
+
+let make_warnings_list = make_events_list false
+
+let gen_section_warnings env =
+ 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.
+ *)
+ let prelude =
+ if env.is_draft then
+ [ Comment "you can comment on each individual error" ]
+ else
+ [
+ Block ( text @@ glue [
+ bold "Important warning:";
+ plain "Frama-C did not complete its execution ";
+ plain "successfully. Analysis results may be inaccurate.";
+ plain ((plural errs "The error") ^ " listed below must be");
+ plain "fixed first before examining other ";
+ plain "warnings and alarms."
+ ] ) ;
+ make_errors_table errs
+ ]
+ in
+ H1 (plain "Errors in the analyzer", Some "errors")
+ :: prelude
+ @ make_errors_list env (List.rev errs)
+ end else []
+ in
+ if Messages.nb_warnings () <> 0 then begin
+ let prelude =
+ if env.is_draft then
+ [Comment "you can comment on each individual error"]
+ else
+ [Block (
+ (text @@ glue [
+ 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 @@ glue [
+ plain "Note that this does not take into account emitted alarms:";
+ plain "they are reported in";
+ link ~text:(plain "the next section") ~name:"alarms" ()
+ ])
+ );
+ make_warnings_table warnings ]
+ in
+ error_section @
+ H1 (plain "Warnings", Some "warnings")
+ :: prelude
+ @ make_warnings_list env (List.rev warnings)
+ end else error_section
+
+let gen_section_alarms env =
+ let treat_alarm e kf s ~rank:_ alarm annot (i, sec, content) =
+ let label = "Alarm-" ^ string_of_int i in
+ let link = link ~text:(format "%d" i) ~name:label () in
+ let kind = code @@ Alarms.get_name alarm in
+ let func = code @@ Kernel_function.get_name kf in
+ 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 ~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
+ Block descr :: insert_marks env label
+ else
+ Block
+ ( (text @@ glue [
+ plain "The following ACSL assertion must hold to avoid" ;
+ plain (Alarms.get_description alarm |> String.lowercase_ascii) ;
+ format "(undefined behavior)."
+ ])
+ @ descr )
+ :: insert_remark env label
+ in
+ (i+1,
+ sec @ H2 (sec_title, Some label) :: sec_content,
+ [ link; kind; emitter; func; loc_text ] :: content)
+ in
+ let _,sections, content = Alarms.fold treat_alarm (0,[],[]) in
+ let content = List.rev content in
+ match content with
+ | [] ->
+ let anchor = "alarms" in
+ let text_content =
+ if env.is_draft then
+ Comment "No alarm!" :: insert_marks env anchor
+ else
+ Block (text @@ glue [
+ bold "No alarm"; plain "was found during the analysis";
+ plain "Any execution starting from";
+ 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."
+ ])
+ :: insert_remark env anchor
+ in
+ H1 (plain "Results of the analysis", Some anchor) :: text_content
+ | _ :: 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 "No", Center;
+ plain "Kind", Center;
+ plain "Emitter", Center;
+ plain "Function", Left;
+ plain "Location", Left;
+ ]
+ in
+ let text_content =
+ if env.is_draft then begin
+ sections
+ end else begin
+ Block (text @@ glue [
+ plain ("The table below lists the " ^ alarm);
+ plain "that have been emitted during the analysis.";
+ plain "Any execution starting from";
+ 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.";
+ plain "More information on each individual alarm is";
+ plain "given in the remainder of this section"
+ ]) ::
+ Table { content; caption; header } ::
+ sections
+ end
+ in
+ H1 (plain "Results of the analysis", Some "alarms") :: text_content
+
+let gen_section_callgraph env =
+ let f = Mdr_params.FlameGraph.get () in
+ if f = "" then []
+ else begin
+ let anchor = "flamegraph" in
+ let content =
+ if env.is_draft then
+ Comment
+ "A flamegraph provides a visualization of the functions and \
+ callstacks whose analysis is the most costly."
+ :: insert_marks env anchor
+ else
+ par (
+ plain "The image below shows the flamegraph (" @
+ url "http://www.brendangregg.com/flamegraphs.html" @
+ plain ") for the chosen entry point."
+ )
+ @ par (image ~alt:"Flamegraph visualization." ~file:f)
+ @ insert_remark env anchor
+ in
+ H1 (plain "Flamegraph", Some anchor) :: content
+ end
+
+let gen_section_postlude env =
+ let anchor = "conclusion" in
+ let header = H1 (plain "Conclusion", Some anchor) in
+ if env.is_draft then
+ header ::
+ Comment "You can put here some concluding remarks"
+ :: insert_marks env anchor
+ else begin
+ match insert_remark env anchor with
+ | [] -> []
+ | (_::_) as l -> header :: l
+ end
+
+let gen_alarms env =
+ gen_section_warnings env @
+ gen_section_alarms env @
+ gen_section_callgraph env @
+ gen_section_postlude env
+
+let mk_remarks is_draft =
+ let f = Mdr_params.Remarks.get () in
+ if f <> "" then Parse_remarks.get_remarks f
+ else if is_draft then begin
+ let f = Mdr_params.Output.get() in
+ if Sys.file_exists f then begin
+ Mdr_params.feedback
+ "Re-using pre-existing remarks in draft file %s" f;
+ Parse_remarks.get_remarks f
+ end else Datatype.String.Map.empty
+ end else Datatype.String.Map.empty
+
+let gen_report ~draft:is_draft () =
+ let remarks = mk_remarks is_draft in
+ let env = { remarks; is_draft } in
+ let context = gen_context env in
+ let coverage = gen_coverage env in
+ let alarms = gen_alarms env in
+ let title = Mdr_params.Title.get () in
+ let title =
+ if title = "" then begin
+ if is_draft then
+ plain "Draft report"
+ else
+ plain "Frama-C Analysis Report"
+ end else plain title
+ in
+ let authors = List.map (fun x -> plain x) (Mdr_params.Authors.get ()) in
+ let date = match Mdr_params.Date.get () with
+ | "" -> None
+ | s -> Some (plain s) in
+ let elements = context @ coverage @ alarms in
+ let elements =
+ if is_draft then
+ 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 pandoc markdown \
+ content between the BEGIN and END comments. In addition, the plug-in \
+ will consider any \\<!-- INCLUDE file.md --\\> comment (without backslashes) \
+ 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
+ else elements
+ in
+ let elements =
+ Raw [ "\\let\\underscore\\_" ;
+ "\\renewcommand{\\_}{\\discretionary{\\underscore}{}{\\underscore}}"]
+ :: elements
+ in
+ let doc = Markdown.pandoc ~title ~authors ?date elements in
+ let file = Mdr_params.Output.get() in
+ try
+ Command.print_file file (fun fmt -> Markdown.pp_pandoc fmt doc) ;
+ Mdr_params.result "Report %s generated" file
+ with Sys_error s ->
+ Mdr_params.warning
+ "Unable to open %s for writing (%s). No report generated" file s
diff --git a/src/plugins/markdown-report/md_gen.mli b/src/plugins/markdown-report/md_gen.mli
new file mode 100644
index 0000000000000000000000000000000000000000..57e15778a51f8e5a27e20612a5030540d7cd8092
--- /dev/null
+++ b/src/plugins/markdown-report/md_gen.mli
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** generates the report (either final or [draft] according to the flag) *)
+val gen_report: draft:bool -> 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..702e8f368db424e0a25eef178f520cb3fc098509
--- /dev/null
+++ b/src/plugins/markdown-report/mdr_params.ml
@@ -0,0 +1,100 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+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 = String(
+ struct
+ let option_name = "-mdr-gen"
+ let arg_name = "kind"
+ let default = "none"
+ let help =
+ "select the <kind> of report to generate among: \
+ none (default), md, draft and sarif"
+ end)
+
+let () =
+ Generate.set_possible_values [ "none"; "md"; "draft"; "sarif" ]
+
+module Remarks = Empty_string(
+ struct
+ let option_name = "-mdr-remarks"
+ let arg_name = "f"
+ let help =
+ "reads file <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 FlameGraph = Empty_string(
+ struct
+ let option_name = "-mdr-flamegraph"
+ let arg_name = "f"
+ let help =
+ "reads file <f> to include a FlameGraph (https://github.com/brendangregg/FlameGraph.git),\
+ allowing the most analysis-intensive callstacks to be identified\
+ quickly and accurately"
+ 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 Title = Empty_string(
+ struct
+ let option_name = "-mdr-title"
+ let arg_name = "t"
+ let help = "title of the generated document"
+ end)
+
+module Date = Empty_string(
+ struct
+ let option_name = "-mdr-date"
+ let arg_name = "d"
+ let help = "date 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..519245e2ce71fd27a5b80a549a0b23debaf920e3
--- /dev/null
+++ b/src/plugins/markdown-report/mdr_params.mli
@@ -0,0 +1,47 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+include Plugin.S
+
+(** Value of [-mdr-out]. *)
+module Output: Parameter_sig.String
+
+(** Value of [-mdr-gen]. *)
+module Generate: Parameter_sig.String
+
+(** Value of [-mdr-remarks]. *)
+module Remarks: Parameter_sig.String
+
+(** Value of [-mdr-flamegraph]. *)
+module FlameGraph: Parameter_sig.String
+
+(** Value of [-mdr-authors]. *)
+module Authors: Parameter_sig.String_list
+
+(** Value of [-mdr-title]. *)
+module Title: Parameter_sig.String
+
+(** Value of [-mdr-date]. *)
+module Date: Parameter_sig.String
+
+(** Value of [-mdr-stubs]. *)
+module Stubs: Parameter_sig.String_list
diff --git a/src/plugins/markdown-report/mdr_register.ml b/src/plugins/markdown-report/mdr_register.ml
new file mode 100644
index 0000000000000000000000000000000000000000..b9e23074135024ed2ee9bc8cfd905cce5f4d1426
--- /dev/null
+++ b/src/plugins/markdown-report/mdr_register.ml
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+let main () =
+ match Mdr_params.Generate.get () with
+ | "none" -> ()
+ | "md" -> Md_gen.gen_report ~draft:false ()
+ | "draft" -> Md_gen.gen_report ~draft:true ()
+ | "sarif" -> Sarif_gen.generate ()
+ | s ->
+ Mdr_params.fatal "Unexpected value for option %s: %s"
+ Mdr_params.Generate.option_name s
+
+let () = Db.Main.extend main
diff --git a/src/plugins/markdown-report/mdr_register.mli b/src/plugins/markdown-report/mdr_register.mli
new file mode 100644
index 0000000000000000000000000000000000000000..001aa5fea6d478fbf31377ad42deaa74a22875e4
--- /dev/null
+++ b/src/plugins/markdown-report/mdr_register.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Registration of the main entry point of the plug-in. Nothing is exported *)
diff --git a/src/plugins/markdown-report/parse_remarks.ml b/src/plugins/markdown-report/parse_remarks.ml
new file mode 100644
index 0000000000000000000000000000000000000000..2cfb092e35f2252a8fa71deb782fcc5d5f199e73
--- /dev/null
+++ b/src/plugins/markdown-report/parse_remarks.ml
@@ -0,0 +1,124 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+type env =
+ { mutable current_section: string;
+ mutable is_markdown: bool;
+ mutable current_markdown: string list;
+ (* markdown lines of current element, in reverse order. *)
+ mutable remarks: Markdown.element list Datatype.String.Map.t }
+
+let dkey = Mdr_params.register_category "remarks"
+
+let empty_env () =
+ { current_section = "";
+ is_markdown = false;
+ current_markdown = [];
+ remarks = Datatype.String.Map.empty }
+
+let add_channel env chan =
+ try
+ while true do
+ let s = input_line chan in
+ env.current_markdown <- s :: env.current_markdown;
+ done;
+ with End_of_file -> ()
+
+let beg_markdown = Str.regexp_string "<!-- BEGIN_REMARK -->"
+
+let end_markdown = Str.regexp_string "<!-- END_REMARK -->"
+
+let include_markdown = Str.regexp "<!-- INCLUDE \\(.*\\) -->"
+
+let is_section = Str.regexp "^#[^{]*{#+\\([^}]*\\)}"
+
+let cleanup_blanks l =
+ let rec aux = function "" :: l -> aux l | l -> l in aux (List.rev (aux l))
+
+let parse_line env line =
+ if env.is_markdown then begin
+ if Str.string_match end_markdown line 0 then begin
+ let remark = cleanup_blanks env.current_markdown in
+ let remark =
+ match remark with
+ | [] ->
+ Mdr_params.debug ~dkey
+ "Empty remark for section %s" env.current_section;
+ []
+ | _ ->
+ let res = Markdown.Raw remark in
+ let page = "" in
+ Mdr_params.debug ~dkey
+ "Remark for section %s:@\n%a"
+ env.current_section (Markdown.pp_element ~page) res;
+ [res]
+ in
+ env.remarks <-
+ Datatype.String.Map.add env.current_section remark env.remarks;
+ env.current_markdown <- [];
+ env.is_markdown <- false
+ end else if Str.string_match include_markdown line 0 then begin
+ let f = Str.matched_group 1 line in
+ Mdr_params.debug ~dkey
+ "Remark for section %s in file %s" env.current_section f;
+ try
+ let chan = open_in f in
+ add_channel env 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
+ env.current_markdown <- line :: env.current_markdown;
+ end
+ end else if Str.string_match beg_markdown line 0 then begin
+ Mdr_params.debug ~dkey
+ "Checking remarks for section %s" env.current_section;
+ env.is_markdown <- true
+ end else if Str.string_match is_section line 0 then begin
+ let sec = Str.matched_group 1 line in
+ Mdr_params.debug ~dkey "Entering section %s" sec;
+ 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 =
+ Mdr_params.debug ~dkey "Using remarks file %s" 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..3ad9877849994848f2809ec91e12c4652347f65a
--- /dev/null
+++ b/src/plugins/markdown-report/parse_remarks.mli
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** 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
diff --git a/src/plugins/markdown-report/sarif.ml b/src/plugins/markdown-report/sarif.ml
new file mode 100644
index 0000000000000000000000000000000000000000..df72f6a1f21ab9fac0a3fef50306e55aa4279ea9
--- /dev/null
+++ b/src/plugins/markdown-report/sarif.ml
@@ -0,0 +1,1036 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** OCaml representation for the sarif 2.0 schema. *)
+
+(** ppx_deriving_yojson generates parser and printer that are recursive
+ by default: we must thus silence spurious let rec warning (39). *)
+[@@@ warning "-39"]
+
+module type Json_type = sig
+ type t
+ val of_yojson: Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
+ val to_yojson: t -> Yojson.Safe.t
+end
+
+module Json_dictionary(J: Json_type):
+ Json_type with type t = (string * J.t) list =
+struct
+ type t = (string * J.t) list
+ let bind x f = match x with Ok x -> f x | Error e -> Error e
+ let bindret x f = bind x (fun x -> Ok (f x))
+ let bind_pair f (s, x) = bindret (f x) (fun x -> (s, x))
+ let one_step f acc x =
+ bind acc (fun acc -> (bindret (f x) (fun x -> (x :: acc))))
+ let bind_list l f =
+ bindret (List.fold_left (one_step (bind_pair f)) (Ok []) l) List.rev
+ let of_yojson = function
+ | `Assoc l ->
+ (match bind_list l J.of_yojson with
+ | Error e -> Error ("dict." ^ e)
+ | Ok _ as res -> res)
+ | `Null -> Ok []
+ | _ -> Error "dict"
+ let to_yojson l =
+ let json_l = List.map (fun (s, x) -> (s, J.to_yojson x)) l in
+ `Assoc json_l
+end
+
+module Uri: sig
+ include Json_type with type t = private string
+ val sarif_github:t
+end
+=
+struct
+ type t = string[@@deriving yojson]
+ let sarif_github =
+ "https://github.com/oasis-tcs/sarif-spec/blob/master/Documents/CommitteeSpecificationDrafts/v2.0-CSD.1/sarif-schema.json"
+end
+
+module Version: sig
+ include Json_type with type t = private string
+ val v2_0_0: t
+end
+=
+struct
+ type t = string[@@deriving yojson]
+ let v2_0_0 = "2.0.0"
+end
+
+module Message = struct
+ type t = {
+ text: (string [@default ""]);
+ messageId: (string [@default ""]);
+ richText: (string [@default ""]);
+ richMessageId: (string [@default ""]);
+ arguments: (string list [@default []]);
+ }[@@deriving yojson]
+
+ let create
+ ?(text="")
+ ?(messageId="")
+ ?(richText="")
+ ?(richMessageId="")
+ ?(arguments=[])
+ ()
+ =
+ { text; messageId; richText; richMessageId; arguments }
+
+ let plain_text ~text ?id:messageId ?arguments () =
+ create ~text ?messageId ?arguments ()
+
+ let markdown ~markdown ?id:richMessageId ?arguments () =
+ let pp fmt = Markdown.pp_elements fmt in
+ let richText = String.trim (Format.asprintf "@[%a@]" pp markdown)
+ in
+ create ~richText ?richMessageId ?arguments ()
+
+ let default = create ()
+end
+
+module FileLocation = struct
+ type t = {
+ uri: string;
+ uriBaseId: (string [@default ""])
+ }[@@deriving yojson]
+
+ let create ~uri ?(uriBaseId = "") () = { uri; uriBaseId }
+
+ let default = create ~uri:"" ()
+
+ let of_loc loc =
+ let open Filepath in
+ (* by construction, we have an absolute path here, no need for uriBase *)
+ let uri = ((fst loc).pos_path :> string) in
+ create ~uri ()
+end
+
+module FileContent = struct
+ type t =
+ | Text of string [@name "text"]
+ | Binary of string [@name "binary"]
+ [@@deriving yojson]
+
+ let default = Text ""
+end
+
+module Region = struct
+ type t = {
+ startLine: (int [@default 0]);
+ startColumn: (int [@default 0]);
+ endLine: (int [@default 0]);
+ endColumn: (int [@default 0]);
+ charOffset: (int [@default 0]);
+ charLength: (int [@default 0]);
+ byteOffset: (int [@default 0]);
+ byteLength: (int [@default 0]);
+ snippet: (FileContent.t [@default FileContent.default]);
+ message: (Message.t [@default Message.default])
+ }[@@deriving yojson]
+
+ let create
+ ?(startLine = 0)
+ ?(startColumn = 0)
+ ?(endLine = 0)
+ ?(endColumn = 0)
+ ?(charOffset = 0)
+ ?(charLength = 0)
+ ?(byteOffset = 0)
+ ?(byteLength = 0)
+ ?(snippet = FileContent.default)
+ ?(message = Message.default)
+ ()
+ =
+ { startLine; startColumn; endLine; endColumn; charOffset; charLength;
+ byteOffset; byteLength; snippet; message }
+
+ let default = create ()
+
+ let of_loc loc =
+ let open Filepath in
+ let (start, finish) = loc in
+ let startLine = start.pos_lnum in
+ let startColumn = start.pos_cnum - start.pos_bol in
+ let endLine = finish.pos_lnum in
+ let endColumn = finish.pos_cnum - finish.pos_bol in
+ let byteLength = finish.pos_cnum - start.pos_cnum in
+ create ~startLine ~startColumn ~endLine ~endColumn ~byteLength ()
+end
+
+module Rectangle = struct
+ type t = {
+ top: (float [@default 0.]);
+ left: (float [@default 0.]);
+ bottom: (float [@default 0.]);
+ right: (float [@default 0.]);
+ message: (Message.t [@default Message.default]);
+ }
+ [@@deriving yojson]
+end
+
+module Custom_properties =
+ Json_dictionary(struct
+ type t = Yojson.Safe.t
+ let of_yojson x = Ok x
+ let to_yojson x = x
+ end)
+
+module Properties = struct
+ type tags = string list [@@deriving yojson]
+
+ type t = {
+ tags: tags;
+ additional_properties: Custom_properties.t
+ }
+
+ let default = { tags = []; additional_properties = [] }
+
+ let create additional_properties =
+ let tags = List.map fst additional_properties in
+ { tags; additional_properties }
+
+ let of_yojson = function
+ | `Null -> Ok default
+ | `Assoc l ->
+ (match List.assoc_opt "tags" l with
+ | None -> Error "properties"
+ | Some json ->
+ (match tags_of_yojson json with
+ | Ok tags ->
+ let additional_properties = List.remove_assoc "tags" l in
+ Ok { tags; additional_properties }
+ | Error loc -> Error ("properties." ^ loc)))
+ | _ -> Error "properties"
+
+ let to_yojson { tags; additional_properties } =
+ match tags with
+ | [] -> `Null
+ | _ -> `Assoc (("tags", tags_to_yojson tags)::additional_properties)
+end
+
+module PhysicalLocation = struct
+ type t = {
+ id: (string [@default ""]);
+ fileLocation: FileLocation.t;
+ region: (Region.t [@default Region.default]);
+ contextRegion: (Region.t [@default Region.default]);
+ }[@@deriving yojson]
+
+ let create
+ ?(id = "")
+ ~fileLocation
+ ?(region = Region.default)
+ ?(contextRegion = Region.default)
+ ()
+ =
+ { id; fileLocation; region; contextRegion }
+
+ let default = create ~fileLocation:FileLocation.default ()
+
+ let of_loc loc =
+ let fileLocation = FileLocation.of_loc loc in
+ let region = Region.of_loc loc in
+ create ~fileLocation ~region ()
+
+end
+
+module Location = struct
+ type t = {
+ physicalLocation: PhysicalLocation.t;
+ fullyQualifiedLogicalName: (string [@default ""]);
+ message: (Message.t [@default Message.default]);
+ annotations: (Region.t list [@default []]);
+ properties: (Properties.t [@default Properties.default]);
+ }[@@deriving yojson]
+
+ let create
+ ~physicalLocation
+ ?(fullyQualifiedLogicalName = "")
+ ?(message = Message.default)
+ ?(annotations = [])
+ ?(properties = Properties.default)
+ ()
+ =
+ { physicalLocation; fullyQualifiedLogicalName;
+ message; annotations; properties;
+ }
+
+ let default = create ~physicalLocation:PhysicalLocation.default ()
+
+ let of_loc loc =
+ let physicalLocation = PhysicalLocation.of_loc loc in
+ create ~physicalLocation ()
+end
+
+module StackFrame = struct
+ type t = {
+ location: (Location.t [@default Location.default]);
+ stack_module: (string [@default ""])[@key "module"];
+ threadId: (int [@default 0]);
+ address: (int [@default 0]);
+ offset: (int [@default 0]);
+ parameters: (string list [@default []]);
+ properties: (Properties.t [@default Properties.default]);
+ }[@@deriving yojson]
+end
+
+module Stack = struct
+ type t = {
+ message: (Message.t [@default Message.default]);
+ frames: StackFrame.t list;
+ properties: (Properties.t [@default Properties.default]);
+ }[@@deriving yojson]
+
+ let default = {
+ message = Message.default;
+ frames = [];
+ properties = Properties.default;
+ }
+end
+
+
+module Additional_properties = struct
+ include Json_dictionary(struct type t = string[@@deriving yojson] end)
+
+ let default = []
+end
+
+module Stl_importance: sig
+ include Json_type with type t = private string
+ val important: t
+ val essential: t
+ val unimportant: t
+end
+=
+struct
+ type t = string [@@deriving yojson]
+ let important = "important"
+ let essential = "essential"
+ let unimportant = "unimportant"
+end
+
+module ThreadFlowLocation = struct
+ type t = {
+ step: int;
+ location: (Location.t [@default Location.default]);
+ stack: (Stack.t [@default Stack.default]);
+ kind: (string [@default ""]);
+ tfl_module: (string [@default ""])[@key "module"];
+ state: (Additional_properties.t [@default Additional_properties.default]);
+ nestingLevel: (int [@default 0]);
+ executionOrder: (int [@default 0]);
+ timestamp: (string [@default ""]);
+ importance: (Stl_importance.t [@default Stl_importance.unimportant]);
+ properties: (Properties.t [@default Properties.default]);
+ }[@@deriving yojson]
+end
+
+module ThreadFlow = struct
+ type t = {
+ id: (string [@default ""]);
+ message: (Message.t [@default Message.default]);
+ locations: ThreadFlowLocation.t list;
+ properties: (Properties.t [@default Properties.default]);
+ }[@@deriving yojson]
+end
+
+module Attachment = struct
+ type t = {
+ description: (Message.t [@default Message.default ]);
+ fileLocation: FileLocation.t;
+ regions: (Region.t list [@default []]);
+ rectangles: (Rectangle.t list [@default []])
+ } [@@deriving yojson]
+end
+
+module CodeFlow = struct
+ type t = {
+ description: (Message.t [@default Message.default]);
+ threadFlows: ThreadFlow.t list;
+ properties: (Properties.t [@default Properties.default]);
+ } [@@deriving yojson]
+end
+
+module Sarif_exception = struct
+ type t = {
+ kind: (string [@default ""]);
+ message: (string [@default ""]);
+ stack: (Stack.t [@default Stack.default]);
+ innerExceptions: (t list [@default []]);
+ }[@@deriving yojson]
+
+ let default =
+ {
+ kind = "";
+ message = "";
+ stack = Stack.default;
+ innerExceptions = []
+ }
+end
+
+module Notification_kind: sig
+ include Json_type with type t = private string
+ val note: t
+ val warning: t
+ val error: t
+end
+=
+struct
+ type t = string [@@deriving yojson]
+ let note = "note"
+ let warning = "warning"
+ let error = "error"
+end
+
+module Notification = struct
+ type t = {
+ id: (string [@default ""]);
+ ruleId: (string [@default ""]);
+ physicalLocation: (PhysicalLocation.t [@default PhysicalLocation.default]);
+ message: Message.t;
+ level: (Notification_kind.t [@default Notification_kind.warning]);
+ threadId: (int [@default 0]);
+ time: (string [@default ""]);
+ exn: (Sarif_exception.t [@default Sarif_exception.default])
+ [@key "exception"];
+ properties: (Properties.t [@default Properties.default])
+ }[@@deriving yojson]
+end
+
+module Tool = struct
+ type t = {
+ name: string;
+ fullName: (string [@default ""]);
+ version: (string [@default ""]);
+ semanticVersion: (string [@default ""]);
+ fileVersion: (string [@default ""]);
+ downloadUri: (string [@default ""]);
+ sarifLoggerVersion: (string [@default ""]);
+ language: (string [@default "en-US"]);
+ properties: (Properties.t [@default Properties.default]);
+ }[@@deriving yojson]
+
+ let create
+ ~name
+ ?(fullName="")
+ ?(version="")
+ ?(semanticVersion="")
+ ?(fileVersion="")
+ ?(downloadUri="")
+ ?(sarifLoggerVersion="")
+ ?(language="en-US")
+ ?(properties=Properties.default)
+ ()
+ =
+ { name; fullName; version; semanticVersion; fileVersion;
+ downloadUri; sarifLoggerVersion; language; properties }
+
+ let default = create ~name:"" ()
+
+end
+
+module Invocation = struct
+
+ type t = {
+ commandLine: string;
+ arguments: string list;
+ responseFiles: (FileLocation.t list [@default []]);
+ attachments: (Attachment.t list [@default []]);
+ startTime: (string [@default ""]);
+ endTime: (string [@default ""]);
+ exitCode: int;
+ toolNotifications: (Notification.t list [@default []]);
+ configurationNotifications: (Notification.t list [@default []]);
+ exitCodeDescription: (string [@default ""]);
+ exitSignalName: (string [@default ""]);
+ exitSignalNumber: (int [@default 0]);
+ processStartFailureMessage: (string [@default ""]);
+ toolExecutionSuccessful: bool;
+ machine: (string [@default ""]);
+ account: (string [@default ""]);
+ processId: (int [@default 0]);
+ executableLocation: (FileLocation.t [@default FileLocation.default]);
+ workingDirectory: (FileLocation.t [@default FileLocation.default]);
+ environmentVariables:
+ (Additional_properties.t [@default Additional_properties.default]);
+ stdin: (FileLocation.t [@default FileLocation.default]);
+ stdout: (FileLocation.t [@default FileLocation.default]);
+ stderr: (FileLocation.t [@default FileLocation.default]);
+ stdoutStderr: (FileLocation.t [@default FileLocation.default]);
+ properties: (Properties.t [@default Properties.default]);
+ }[@@deriving yojson]
+
+ let create
+ ~commandLine
+ ?(arguments = [])
+ ?(responseFiles = [])
+ ?(attachments = [])
+ ?(startTime = "")
+ ?(endTime = "")
+ ?(exitCode = 0)
+ ?(toolNotifications = [])
+ ?(configurationNotifications = [])
+ ?(exitCodeDescription = "")
+ ?(exitSignalName = "")
+ ?(exitSignalNumber = 0)
+ ?(processStartFailureMessage = "")
+ ?(toolExecutionSuccessful = true)
+ ?(machine = "")
+ ?(account = "")
+ ?(processId = 0)
+ ?(executableLocation = FileLocation.default)
+ ?(workingDirectory = FileLocation.default)
+ ?(environmentVariables = Additional_properties.default)
+ ?(stdin = FileLocation.default)
+ ?(stdout = FileLocation.default)
+ ?(stderr = FileLocation.default)
+ ?(stdoutStderr = FileLocation.default)
+ ?(properties = Properties.default)
+ ()
+ =
+ {
+ commandLine;
+ arguments;
+ responseFiles;
+ attachments;
+ startTime;
+ endTime;
+ exitCode;
+ toolNotifications;
+ configurationNotifications;
+ exitCodeDescription;
+ exitSignalName;
+ exitSignalNumber;
+ processStartFailureMessage;
+ toolExecutionSuccessful;
+ machine;
+ account;
+ processId;
+ executableLocation;
+ workingDirectory;
+ environmentVariables;
+ stdin;
+ stdout;
+ stderr;
+ stdoutStderr;
+ properties;
+ }
+
+ let default = create ~commandLine:"/bin/true" ()
+
+end
+
+module Conversion = struct
+ type t = {
+ tool: Tool.t;
+ invocation: (Invocation.t [@default Invocation.default]);
+ analysisToolLogFiles: (FileLocation.t [@default FileLocation.default]);
+ } [@@deriving yojson]
+
+ let default = {
+ tool = Tool.default;
+ invocation = Invocation.default;
+ analysisToolLogFiles = FileLocation.default;
+ }
+end
+
+module Edge = struct
+ type t = {
+ id: string;
+ label: (Message.t [@default Message.default]);
+ sourceNodeId: string;
+ targetNodeId: string;
+ properties: (Properties.t [@default Properties.default])
+ } [@@deriving yojson]
+end
+
+module Node = struct
+ type t = {
+ id: string;
+ label: (string [@default ""]);
+ location: (Location.t [@default Location.default]);
+ children: (t list [@default []]);
+ properties: (Properties.t [@default Properties.default]);
+ }[@@deriving yojson]
+end
+
+module Edge_traversal = struct
+ type t = {
+ edgeId: string;
+ message: (Message.t [@default Message.default]);
+ finalState:
+ (Additional_properties.t [@default Additional_properties.default]);
+ stepOverEdgeCount: (int [@default 0]);
+ properties: (Properties.t [@default Properties.default]);
+ }[@@deriving yojson]
+end
+
+module Role: sig
+ include Json_type with type t = private string
+ val analysisTarget: t
+ val attachment: t
+ val responseFile: t
+ val resultFile: t
+ val standardStream: t
+ val traceFile: t
+ val unmodifiedFile: t
+ val modifiedFile: t
+ val addedFile: t
+ val deletedFile:t
+ val renamedFile:t
+ val uncontrolledFile: t
+end
+=
+struct
+ type t = string[@@deriving yojson]
+
+ let analysisTarget = "analysisTarget"
+ let attachment = "attachment"
+ let responseFile = "responseFile"
+ let resultFile = "resultFile"
+ let standardStream = "standardStream"
+ let traceFile = "traceFile"
+ let unmodifiedFile = "unmodifiedFile"
+ let modifiedFile = "modifiedFile"
+ let addedFile = "addedFile"
+ let deletedFile = "deletedFile"
+ let renamedFile = "renamedFile"
+ let uncontrolledFile = "uncontrolledFile"
+end
+
+module Hash = struct
+ type t = {
+ value: string;
+ algorithm: string
+ } [@@deriving yojson]
+end
+
+module Graph = struct
+ type t = {
+ id : string;
+ description: (Message.t [@default Message.default]);
+ nodes: Node.t list;
+ edges: Edge.t list;
+ properties: (Properties.t [@default Properties.default]);
+ }[@@deriving yojson]
+end
+
+module Graph_dictionary = Json_dictionary(Graph)
+
+module GraphTraversal = struct
+ type t = {
+ graphId: string;
+ description: (Message.t [@default Message.default]);
+ initialState:
+ (Additional_properties.t [@default Additional_properties.default]);
+ edgeTraversals: Edge_traversal.t list;
+ properties: (Properties.t [@default Properties.default]);
+ }[@@deriving yojson]
+end
+
+module Replacement = struct
+ type t = {
+ deletedRegion: Region.t;
+ insertedContent: (FileContent.t [@default FileContent.default])
+ }[@@deriving yojson]
+end
+
+module File = struct
+ type t = {
+ fileLocation: (FileLocation.t [@default FileLocation.default]);
+ parentKey: (string [@default ""]);
+ offset: (int [@default 0]);
+ length: (int [@default 0]);
+ roles: (Role.t list [@default []]);
+ mimeType: (string [@default ""]);
+ contents: (FileContent.t [@default FileContent.default]);
+ encoding: (string [@default ""]);
+ hashes: (Hash.t list [@default []]);
+ lastModifiedTime: (string [@default ""]);
+ properties: (Properties.t [@default Properties.default]);
+ }[@@deriving yojson]
+
+ let create
+ ?(fileLocation = FileLocation.default)
+ ?(parentKey = "")
+ ?(offset = 0)
+ ?(length = 0)
+ ?(roles = [])
+ ?(mimeType = "")
+ ?(contents = FileContent.default)
+ ?(encoding = "")
+ ?(hashes = [])
+ ?(lastModifiedTime = "")
+ ?(properties = Properties.default)
+ ()
+ =
+ {
+ fileLocation; parentKey; offset; length; roles; mimeType; contents;
+ encoding; hashes; lastModifiedTime; properties
+ }
+end
+
+module FileChange = struct
+ type t = {
+ fileLocation: FileLocation.t;
+ replacements: Replacement.t list
+ }[@@deriving yojson]
+end
+
+module Fix = struct
+ type t = {
+ description: (Message.t [@defaut Message.default]);
+ fileChanges: FileChange.t list;
+ }[@@deriving yojson]
+end
+
+module ExternalFiles = struct
+ type t = {
+ conversion: (FileLocation.t [@default FileLocation.default]);
+ files: (FileLocation.t [@default FileLocation.default]);
+ graphs: (FileLocation.t [@default FileLocation.default]);
+ invocations: (FileLocation.t list [@default []]);
+ logicalLocations: (FileLocation.t [@default FileLocation.default]);
+ resources: (FileLocation.t [@default FileLocation.default]);
+ results: (FileLocation.t [@default FileLocation.default]);
+ }[@@deriving yojson]
+end
+
+module LogicalLocation = struct
+ type t = {
+ name: string;
+ fullyQualifiedName: string;
+ decoratedName: string;
+ parentKey: string;
+ kind: string;
+ }[@@deriving yojson]
+end
+
+module RuleConfigLevel:
+sig
+ include Json_type with type t = private string
+ val cl_note: t
+ val cl_warning: t
+ val cl_error: t
+ val cl_open: t
+end
+=
+struct
+ type t = string [@@deriving yojson]
+ let cl_note = "note"
+ let cl_warning = "warning"
+ let cl_error = "error"
+ let cl_open = "open"
+end
+
+module RuleConfiguration = struct
+ type t = {
+ enabled: (bool [@default false]);
+ defaultLevel: (RuleConfigLevel.t [@default RuleConfigLevel.cl_open]);
+ parameters: (Properties.t [@default Properties.default])
+ }[@@deriving yojson]
+
+ let default = {
+ enabled = false;
+ defaultLevel = RuleConfigLevel.cl_open;
+ parameters = Properties.default;
+ }
+end
+
+module Rule = struct
+ type t = {
+ id: (string [@default ""]);
+ name: (string [@default ""]);
+ shortDescription: (Message.t [@default Message.default]);
+ fullDescription: (Message.t [@default Message.default]);
+ messageStrings:
+ (Additional_properties.t [@default Additional_properties.default]);
+ richMessageStrings:
+ (Additional_properties.t [@default Additional_properties.default]);
+ configuration: (RuleConfiguration.t [@default RuleConfiguration.default]);
+ helpUri: (string [@default ""]);
+ properties: (Properties.t [@default Properties.default]);
+ }[@@deriving yojson]
+
+ let default = {
+ id = "";
+ name = "";
+ shortDescription = Message.default;
+ fullDescription = Message.default;
+ messageStrings = Additional_properties.default;
+ richMessageStrings = Additional_properties.default;
+ configuration = RuleConfiguration.default;
+ helpUri = "";
+ properties = Properties.default;
+ }
+
+ let create
+ ~id
+ ?(name="")
+ ?(shortDescription=Message.default)
+ ?(fullDescription=Message.default)
+ ?(messageStrings=Additional_properties.default)
+ ?(richMessageStrings=Additional_properties.default)
+ ?(configuration=RuleConfiguration.default)
+ ?(helpUri="")
+ ?(properties=Properties.default)
+ ()
+ =
+ { id; name; shortDescription; fullDescription; messageStrings;
+ richMessageStrings; configuration; helpUri; properties }
+
+end
+
+module Rule_dictionary = Json_dictionary(Rule)
+
+module Resources = struct
+ type t = {
+ messageStrings:
+ (Additional_properties.t [@default Additional_properties.default]);
+ rules: (Rule_dictionary.t [@default []]);
+ }[@@deriving yojson]
+
+ let default = {
+ messageStrings = Additional_properties.default;
+ rules = [] }
+
+ let create
+ ?(messageStrings=Additional_properties.default)
+ ?(rules=[])
+ ()
+ =
+ { messageStrings; rules }
+end
+
+module Result_level:
+sig
+ type t = private string
+ val notApplicable: t
+ val pass: t
+ val note: t
+ val warning: t
+ val error: t
+
+ val to_yojson: t -> Yojson.Safe.t
+ val of_yojson: Yojson.Safe.t -> (t,string) result
+end
+=
+struct
+ type t = string[@@deriving yojson]
+ let notApplicable = "notApplicable"
+ let pass = "pass"
+ let note = "note"
+ let warning = "warning"
+ let error = "error"
+end
+
+module Result_suppressionState: sig
+ include Json_type with type t = private string
+ val suppressedInSource: t
+ val suppressedExternally: t
+end
+=
+struct
+ type t = string [@@deriving yojson]
+ let suppressedInSource = "suppressedInSource"
+ let suppressedExternally = "suppressedExternally"
+end
+
+module Result_baselineState: sig
+ include Json_type with type t = private string
+ val bs_new: t
+ val bs_existing: t
+ val bs_absent: t
+end
+=
+struct
+ type t = string [@@deriving yojson]
+ let bs_new = "new"
+ let bs_existing = "existing"
+ let bs_absent = "absent"
+end
+
+(* we can't use Result here, as this would conflict with
+ Ppx_deriving_yojson_runtime.Result that is opened by the
+ code generated by Ppx_deriving_yojson. *)
+module Sarif_result = struct
+ type t = {
+ ruleId: (string [@default ""]);
+ level: (Result_level.t[@default Result_level.notApplicable]);
+ message: (Message.t [@default Message.default]);
+ analysisTarget: (FileLocation.t [@default FileLocation.default]);
+ locations: (Location.t list [@default []]);
+ instanceGuid: (string [@default ""]);
+ correlationGuid: (string [@default ""]);
+ occurrenceCount: (int [@default 1]);
+ partialFingerprints:
+ (Additional_properties.t [@default Additional_properties.default]);
+ fingerprints:
+ (Additional_properties.t [@default Additional_properties.default]);
+ stacks: (Stack.t list [@default []]);
+ codeFlows: (CodeFlow.t list [@default []]);
+ graphs: (Graph_dictionary.t [@default []]);
+ graphTraversals: (GraphTraversal.t list [@default []]);
+ relatedLocations: (Location.t list [@default []]);
+ suppressionStates: (Result_suppressionState.t list [@default []]);
+ baselineState:
+ (Result_baselineState.t [@default Result_baselineState.bs_absent]);
+ attachments: (Attachment.t list [@default []]);
+ workItemsUris: (string list [@default []]);
+ conversionProvenance: (PhysicalLocation.t list [@default[]]);
+ fixes: (Fix.t list [@default []]);
+ properties: (Properties.t [@default Properties.default])
+ }[@@deriving yojson]
+
+ let create
+ ?(ruleId = "")
+ ?(level=Result_level.notApplicable)
+ ?(message=Message.default)
+ ?(analysisTarget=FileLocation.default)
+ ?(locations=[])
+ ?(instanceGuid="")
+ ?(correlationGuid="")
+ ?(occurrenceCount=1)
+ ?(partialFingerprints=Additional_properties.default)
+ ?(fingerprints=Additional_properties.default)
+ ?(stacks=[])
+ ?(codeFlows=[])
+ ?(graphs=[])
+ ?(graphTraversals=[])
+ ?(relatedLocations=[])
+ ?(suppressionStates=[])
+ ?(baselineState=Result_baselineState.bs_absent)
+ ?(attachments=[])
+ ?(workItemsUris=[])
+ ?(conversionProvenance=[])
+ ?(fixes=[])
+ ?(properties=Properties.default)
+ ()
+ =
+ {
+ ruleId;level; message; analysisTarget; locations; instanceGuid;
+ correlationGuid; occurrenceCount; partialFingerprints; fingerprints;
+ stacks; codeFlows; graphs; graphTraversals; relatedLocations;
+ suppressionStates; baselineState; attachments; workItemsUris;
+ conversionProvenance; fixes; properties
+ }
+end
+
+module VersionControlDetails = struct
+ type t = {
+ uri: string;
+ revisionId: (string [@default ""]);
+ branch: (string [@default ""]);
+ tag: (string [@default ""]);
+ timestamp: (string [@default ""]);
+ properties: (Properties.t [@default Properties.default]);
+ }[@@deriving yojson]
+end
+
+module File_dictionary = Json_dictionary(File)
+
+module LogicalLocation_dictionary = Json_dictionary(LogicalLocation)
+
+module ColumnKind: sig
+ include Json_type with type t = private string
+ val utf16CodeUnits: t
+ val unicodeCodePoints: t
+end
+=
+struct
+ type t = string [@@deriving yojson]
+ let utf16CodeUnits = "utf16CodeUnits"
+ let unicodeCodePoints = "unicodeCodePoints"
+end
+
+module Run = struct
+ type t = {
+ tool: Tool.t;
+ invocations: (Invocation.t list [@default []]);
+ conversion: (Conversion.t [@default Conversion.default]);
+ versionControlProvenance: (VersionControlDetails.t list [@default []]);
+ originalUriBaseIds:
+ (Additional_properties.t [@default Additional_properties.default]);
+ files: (File_dictionary.t [@default []]);
+ logicalLocations: (LogicalLocation_dictionary.t [@default []]);
+ graphs: (Graph_dictionary.t [@default []]);
+ results: (Sarif_result.t list [@default []]);
+ resources: (Resources.t [@default Resources.default]);
+ instanceGuid: (string [@default ""]);
+ correlationGuid: (string [@default ""]);
+ logicalId: (string [@default ""]);
+ description: (Message.t [@default Message.default]);
+ automationLogicalId: (string [@default ""]);
+ baselineInstanceGuid: (string [@default ""]);
+ architecture: (string [@default ""]);
+ richMessageMimeType: (string [@default "text/markdown;variant=GFM" ]);
+ redactionToken: (string [@default ""]);
+ defaultFileEncoding: (string [@default "utf-8"]);
+ columnKind: (ColumnKind.t [@default ColumnKind.unicodeCodePoints]);
+ properties: (Properties.t [@default Properties.default]);
+ }
+ [@@deriving yojson]
+
+ let create
+ ~tool
+ ~invocations
+ ?(conversion=Conversion.default)
+ ?(versionControlProvenance=[])
+ ?(originalUriBaseIds=Additional_properties.default)
+ ?(files=[])
+ ?(logicalLocations=[])
+ ?(graphs=[])
+ ?(results=[])
+ ?(resources=Resources.default)
+ ?(instanceGuid="")
+ ?(correlationGuid="")
+ ?(logicalId="")
+ ?(description=Message.default)
+ ?(automationLogicalId="")
+ ?(baselineInstanceGuid="")
+ ?(architecture="")
+ ?(richMessageMimeType="text/markdown;variant=GFM")
+ ?(redactionToken="")
+ ?(defaultFileEncoding="utf-8")
+ ?(columnKind=ColumnKind.unicodeCodePoints)
+ ?(properties=Properties.default)
+ ()
+ =
+ {
+ tool; invocations; conversion; versionControlProvenance; originalUriBaseIds;
+ files; logicalLocations; graphs; results; resources; instanceGuid;
+ correlationGuid; logicalId; description; automationLogicalId;
+ baselineInstanceGuid; architecture; richMessageMimeType;
+ redactionToken; defaultFileEncoding; columnKind; properties
+ }
+end
+
+module Schema = struct
+ type t = {
+ schema: (Uri.t [@default Uri.sarif_github]) [@key "$schema"];
+ version: Version.t;
+ runs: Run.t list
+ } [@@deriving yojson]
+
+ let create ?(schema=Uri.sarif_github) ?(version=Version.v2_0_0) ~runs () =
+ { schema; version; runs }
+end
diff --git a/src/plugins/markdown-report/sarif_gen.ml b/src/plugins/markdown-report/sarif_gen.ml
new file mode 100644
index 0000000000000000000000000000000000000000..f06371ecf1cef5d6616496a6cc449709c78787c8
--- /dev/null
+++ b/src/plugins/markdown-report/sarif_gen.ml
@@ -0,0 +1,193 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Sarif
+
+let frama_c_sarif =
+ let name = "frama-c" in
+ let version = Config.version_and_codename in
+ let semanticVersion = Config.version in
+ let fullName = name ^ "-" ^ version in
+ let downloadUri = "https://frama-c.com/download.html" in
+ Tool.create
+ ~name ~version ~semanticVersion ~fullName ~downloadUri ()
+
+
+let get_remarks () =
+ let f = Mdr_params.Remarks.get () in
+ if f <> "" then Parse_remarks.get_remarks f
+ else Datatype.String.Map.empty
+
+let get_remark remarks label =
+ match Datatype.String.Map.find_opt label remarks with
+ | None -> []
+ | Some l -> l
+
+let command_line () = Array.to_list Sys.argv
+
+module Analysis_cmdline =
+ State_builder.Ref(Datatype.List(Datatype.String))
+ (struct
+ let name = "Sarif_gen.Analysis_cmdline"
+ let dependencies = []
+ let default = command_line
+ end)
+
+let gen_invocation () =
+ let cl = Analysis_cmdline.get () in
+ let commandLine = String.concat " " cl in
+ let arguments = List.tl cl in
+ Invocation.create ~commandLine ~arguments ()
+
+let gen_remark alarm =
+ let open Markdown in
+ [ Block
+ [ Text
+ (plain
+ (Printf.sprintf "This alarms represents a potential %s."
+ (Alarms.get_description alarm)
+ )
+ )
+ ]
+ ]
+
+let level_of_status =
+ let open Property_status.Feedback in
+ let open Sarif.Result_level in
+ function
+ | Never_tried -> notApplicable
+ | Considered_valid | Valid | Valid_under_hyp | Valid_but_dead -> pass
+ | Unknown | Unknown_but_dead -> warning
+ | Invalid | Invalid_under_hyp | Invalid_but_dead -> error
+ | Inconsistent -> note
+
+let make_message alarm annot remark =
+ let open Markdown in
+ let name = Alarms.get_name alarm in
+ let text = name ^ "." in
+ let kind = plain (name ^ ":") 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
+ | [] -> summary :: gen_remark alarm
+ | _ -> summary :: remark
+ in
+ let richText =
+ String.trim
+ (Format.asprintf "@[%a@]" (Markdown.pp_elements ~page:"") markdown)
+ in
+ Message.create ~text ~richText ()
+
+let gen_results remarks =
+ let treat_alarm _e kf s ~rank:_ alarm annot (i, rules, content) =
+ let prop = Property.ip_of_code_annot_single kf s annot in
+ let ruleId = Alarms.get_name alarm in
+ let rules =
+ Datatype.String.Map.add ruleId (Alarms.get_description alarm) rules
+ in
+ let label = "Alarm-" ^ string_of_int i in
+ let level = level_of_status (Property_status.Feedback.get prop) in
+ let remark = get_remark remarks label in
+ let message = make_message alarm annot remark in
+ let locations = [ Location.of_loc (Cil_datatype.Stmt.loc s) ] in
+ let res =
+ Sarif_result.create ~level ~ruleId ~message ~locations ()
+ in
+ (i+1, rules, res :: content)
+ in
+ let _, rules, content =
+ Alarms.fold treat_alarm (0, Datatype.String.Map.empty,[])
+ in
+ rules, List.rev content
+
+let is_alarm = function
+ | Property.(IPCodeAnnot { ica_ca }) -> Extlib.has_some (Alarms.find ica_ca)
+ | _ -> false
+
+let make_ip_message ip =
+ let text = Format.asprintf "@[%a.@]" Property.short_pretty ip in
+ Message.plain_text ~text ()
+
+let gen_status ip =
+ let status = Property_status.Feedback.get ip in
+ let level = level_of_status status in
+ let locations = [ Location.of_loc (Property.location ip) ] in
+ let message = make_ip_message ip in
+ Sarif_result.create ~level ~locations ~message ()
+
+let gen_statuses () =
+ let f ip content =
+ if is_alarm ip then content else (gen_status ip) :: content
+ in
+ List.rev (Property_status.fold f [])
+
+let gen_files () =
+ let add_src_file f =
+ let key = Filename.chop_extension (Filename.basename f) in
+ let fileLocation = FileLocation.create ~uri:(Filepath.normalize f) () in
+ let roles = [ Role.analysisTarget ] in
+ let mimeType = "text/x-csrc" in
+ key, File.create ~fileLocation ~roles ~mimeType ()
+ in
+ List.map add_src_file (Kernel.Files.get ())
+
+let add_rule id desc l =
+ let text = desc ^ "." in
+ let shortDescription = Message.plain_text ~text () in
+ let rule = Rule.create ~id ~shortDescription () in
+ (id, rule) :: l
+
+let make_rule_dictionary rules = Datatype.String.Map.fold add_rule rules []
+
+let gen_run remarks =
+ let tool = frama_c_sarif in
+ let invocations = [gen_invocation ()] in
+ let rules, results = gen_results remarks in
+ let user_annot_results = gen_statuses () in
+ let rules =
+ match user_annot_results with
+ | [] -> rules
+ | _ ->
+ Datatype.String.Map.add
+ "user-spec" "User written ACSL specification" rules
+ in
+ let rules = make_rule_dictionary rules in
+ let resources = Resources.create ~rules () in
+ let results = results @ user_annot_results in
+ let files = gen_files () in
+ Run.create ~tool ~invocations ~results ~resources ~files ()
+
+let generate () =
+ let remarks = get_remarks () in
+ let runs = [ gen_run remarks ] in
+ let json = Schema.create ~runs () |> Schema.to_yojson in
+ let file = Mdr_params.Output.get () in
+ if file = "" then
+ Log.print_on_output (fun fmt -> Yojson.Safe.pretty_print fmt json)
+ else
+ try
+ Command.write_file file
+ (fun out -> Yojson.Safe.pretty_to_channel ~std:true out json) ;
+ Mdr_params.result "Report %s generated" file
+ with Sys_error s ->
+ Mdr_params.abort "Unable to generate %s (%s)" file s
diff --git a/src/plugins/markdown-report/sarif_gen.mli b/src/plugins/markdown-report/sarif_gen.mli
new file mode 100644
index 0000000000000000000000000000000000000000..84592ecbe2d78af92af43d91f6f30e87e9f7e031
--- /dev/null
+++ b/src/plugins/markdown-report/sarif_gen.mli
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** generate a sarif json object. *)
+val generate: unit -> unit
diff --git a/src/plugins/markdown-report/share/acsl.xml b/src/plugins/markdown-report/share/acsl.xml
new file mode 100644
index 0000000000000000000000000000000000000000..385976a8cf95a2f0215d0ae2919c25c613eb251a
--- /dev/null
+++ b/src/plugins/markdown-report/share/acsl.xml
@@ -0,0 +1,84 @@
+<!---------------------------------------------------------------------------->
+<!-- -->
+<!-- This file is part of Frama-C. -->
+<!-- -->
+<!-- Copyright (C) 2007-2019 -->
+<!-- CEA (Commissariat à l'énergie atomique et aux énergies -->
+<!-- alternatives) -->
+<!-- -->
+<!-- you can redistribute it and/or modify it under the terms of the GNU -->
+<!-- Lesser General Public License as published by the Free Software -->
+<!-- Foundation, version 2.1. -->
+<!-- -->
+<!-- It is distributed in the hope that it will be useful, -->
+<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of -->
+<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -->
+<!-- GNU Lesser General Public License for more details. -->
+<!-- -->
+<!-- See the GNU Lesser General Public License version 2.1 -->
+<!-- for more details (enclosed in the file licenses/LGPLv2.1). -->
+<!-- -->
+<!---------------------------------------------------------------------------->
+
+<?xml version="1.0" encoding="UTF-8"?>
+<language name="ACSL" version="1" extensions="*.acsl"
+ section="Sources" kateversion="2.4">
+<highlighting>
+<list name="keywords">
+<item>allocates</item>
+<item>assert</item>
+<item>assigns</item>
+<item>assumes</item>
+<item>axiom</item>
+<item>axiomatic</item>
+<item>behavior</item>
+<item>behaviors</item>
+<item>boolean</item>
+<item>breaks</item>
+<item>complete</item>
+<item>continues</item>
+<item>data</item>
+<item>decreases</item>
+<item>disjoint</item>
+<item>ensures</item>
+<item>exit_behavior</item>
+<item>frees</item>
+<item>ghost</item>
+<item>global</item>
+<item>inductive</item>
+<item>integer</item>
+<item>invariant</item>
+<item>lemma</item>
+<item>logic</item>
+<item>loop</item>
+<item>model</item>
+<item>predicate</item>
+<item>reads</item>
+<item>real</item>
+<item>requires</item>
+<item>returns</item>
+<item>sizeof</item>
+<item>strong</item>
+<item>struct</item>
+<item>terminates</item>
+<item>type</item>
+<item>union</item>
+<item>variant</item>
+</list>
+<contexts>
+ <context attribute="Normal Text" lineEndContext="#pop" name="Normal Text">
+ <keyword attribute="Keyword" context="#stay" String="keywords"/>
+ <DetectChar attribute="Keyword" context="bskeyword" char="\"/>
+ </context>
+ <context name="bskeyword" attribute="Keyword" lineEndContext="#pop">
+ <DetectIdentifier attribute="Keyword" context="#pop" />
+ </context>
+</contexts>
+<itemDatas>
+ <itemData name="Normal Text" defStyleNum="dsNormal"/>
+ <itemData name="Keyword" defStyleNum="dsKeyword"/>
+</itemDatas>
+<general>
+</general>
+</highlighting>
+</language>
diff --git a/src/plugins/markdown-report/tests/eva/cwe126.c b/src/plugins/markdown-report/tests/eva/cwe126.c
new file mode 100644
index 0000000000000000000000000000000000000000..092f7b27f2105019614987e305524577d61cf350
--- /dev/null
+++ b/src/plugins/markdown-report/tests/eva/cwe126.c
@@ -0,0 +1,94 @@
+/* run.config
+ OPT: -mdr-remarks tests/eva/cwe126.remarks.md
+ */
+
+/* extracted from Juliet test suite v1.3 for C
+ https://samate.nist.gov/SRD/view_testcase.php?tID=76270
+*/
+
+#include <stdlib.h>
+#include <string.h>
+
+void CWE126_Buffer_Overread__malloc_char_loop_64b_badSink(void * dataVoidPtr)
+{
+ /* cast void pointer to a pointer of the appropriate type */
+ char * * dataPtr = (char * *)dataVoidPtr;
+ /* dereference dataPtr into data */
+ char * data = (*dataPtr);
+ {
+ size_t i, destLen;
+ char dest[100];
+ memset(dest, 'C', 100-1);
+ dest[100-1] = '\0'; /* null terminate */
+ destLen = strlen(dest);
+ /* POTENTIAL FLAW: using length of the dest where data
+ * could be smaller than dest causing buffer overread */
+ for (i = 0; i < destLen; i++)
+ {
+ dest[i] = data[i];
+ }
+ dest[100-1] = '\0';
+ free(data);
+ }
+}
+
+void CWE126_Buffer_Overread__malloc_char_loop_64_bad()
+{
+ char * data;
+ data = NULL;
+ /* FLAW: Use a small buffer */
+ data = (char *)malloc(50*sizeof(char));
+ if (data == NULL) {exit(-1);}
+ memset(data, 'A', 50-1); /* fill with 'A's */
+ data[50-1] = '\0'; /* null terminate */
+ CWE126_Buffer_Overread__malloc_char_loop_64b_badSink(&data);
+}
+
+/* goodG2B uses the GoodSource with the BadSink */
+void CWE126_Buffer_Overread__malloc_char_loop_64b_goodG2BSink(void * dataVoidPtr)
+{
+ /* cast void pointer to a pointer of the appropriate type */
+ char * * dataPtr = (char * *)dataVoidPtr;
+ /* dereference dataPtr into data */
+ char * data = (*dataPtr);
+ {
+ size_t i, destLen;
+ char dest[100];
+ memset(dest, 'C', 100-1);
+ dest[100-1] = '\0'; /* null terminate */
+ destLen = strlen(dest);
+ /* POTENTIAL FLAW: using length of the dest where data
+ * could be smaller than dest causing buffer overread */
+ for (i = 0; i < destLen; i++)
+ {
+ dest[i] = data[i];
+ }
+ dest[100-1] = '\0';
+ free(data);
+ }
+}
+
+static void goodG2B()
+{
+ char * data;
+ data = NULL;
+ /* FIX: Use a large buffer */
+ data = (char *)malloc(100*sizeof(char));
+ if (data == NULL) {exit(-1);}
+ memset(data, 'A', 100-1); /* fill with 'A's */
+ data[100-1] = '\0'; /* null terminate */
+ CWE126_Buffer_Overread__malloc_char_loop_64b_goodG2BSink(&data);
+}
+
+void CWE126_Buffer_Overread__malloc_char_loop_64_good()
+{
+ goodG2B();
+}
+
+int main(int argc, char * argv[])
+{
+ CWE126_Buffer_Overread__malloc_char_loop_64_good();
+ CWE126_Buffer_Overread__malloc_char_loop_64_bad();
+ return 0;
+}
+
diff --git a/src/plugins/markdown-report/tests/eva/cwe126.remarks.md b/src/plugins/markdown-report/tests/eva/cwe126.remarks.md
new file mode 100644
index 0000000000000000000000000000000000000000..9e40167cfed25932494165b9044ea105c4081d67
--- /dev/null
+++ b/src/plugins/markdown-report/tests/eva/cwe126.remarks.md
@@ -0,0 +1,131 @@
+---
+title: Draft report
+author:
+date: 2019-10-25
+...
+
+\let\underscore\_
+\renewcommand{\_}{\discretionary{\underscore}{}{\underscore}}
+
+<!-- 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 pandoc markdown content
+ between the BEGIN and END comments. In addition, the plug-in will
+ consider any \<!-- INCLUDE file.md --\> comment (without backslashes) 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.
+-->
+
+# Introduction {#intro}
+
+<!-- You can add here some overall introduction to the analysis -->
+
+<!-- BEGIN_REMARK -->
+
+This is a test from the Juliet test suite showing an example of buffer
+overflow (CWE126). The `good` functions should not trigger any alarm, while
+the `bad` ones have indeed an error.
+
+<!-- END_REMARK -->
+
+# Context of the analysis {#context}
+
+## Input files {#c-input}
+
+<!-- You can add here some remarks about the set of files that is considered
+ by Frama-C
+-->
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+The C source files (not including the headers `.h` files)
+that have been considered during the analysis are the following:
+
+* `./*.c`
+
+
+
+## Configuration {#options}
+
+<!-- You can add here some remarks about the options used for the analysis
+-->
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+### EVA Domains {#domains}
+
+<!-- You can give more information about the choice of EVA domains -->
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+### Stubbed Functions {#stubs}
+
+<!-- You can add here general comments about the stubs that have been used
+-->
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+<!-- No stubs have been used -->
+
+# Coverage {#coverage}
+
+There are 6 function definitions that are not stubbed. They represent 50 statements, of which 50 are potentially reachable through EVA, resulting in a **statement coverage of 100.0%** with respect to the entire application.
+
+
+There were potentially 6 functions syntactically reachable from main.
+These functions contain 50 statements, of which 50 are potentially reachable according to EVA, resulting in a **statement coverage of 100.0%** with respect to the perimeter set by this entry point.
+
+
+<!-- You can comment on the coverage obtained by EVA -->
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+# Warnings {#warnings}
+
+<!-- you can comment on each individual error -->
+
+## Warning 0 (cwe126.c:24) {#warn-0}
+
+```log
+Message: out of bounds read. assert \valid_read(data + i);
+```
+
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+# Results of the analysis {#alarms}
+
+## Alarm 0 at cwe126.c:24 {#Alarm-0}
+
+```acsl
+assert mem_access: \valid_read(data + i);
+```
+
+
+<!-- BEGIN_REMARK -->
+
+This alarm is real: Eva correctly identified the issue and did not report
+any spurious alarm anywhere else.
+
+<!-- END_REMARK -->
+
+# Conclusion {#conclusion}
+
+<!-- You can put here some concluding remarks -->
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
\ No newline at end of file
diff --git a/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md b/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md
new file mode 100644
index 0000000000000000000000000000000000000000..b96d202aea52fd78e9f83eba955b70c5915354fa
--- /dev/null
+++ b/src/plugins/markdown-report/tests/eva/oracle/cwe126.0.md
@@ -0,0 +1,105 @@
+---
+title: Frama-C Analysis Report
+author:
+date: now
+...
+
+\let\underscore\_
+\renewcommand{\_}{\discretionary{\underscore}{}{\underscore}}
+
+# Introduction {#intro}
+
+This is a test from the Juliet test suite showing an example of buffer
+overflow (CWE126). The `good` functions should not trigger any alarm, while
+the `bad` ones have indeed an error.
+
+# Context of the analysis {#context}
+
+## Input files {#c-input}
+
+The C source files (not including the headers `.h` files)
+that have been considered during the analysis are the following:
+
+* `tests/eva/*.c`
+
+
+
+## Configuration {#options}
+
+### EVA Domains {#domains}
+
+Only the base domain (`Cvalue`) has been used for the analysis
+
+
+### Stubbed Functions {#stubs}
+
+No stubs have been used for this analysis
+
+
+# Coverage {#coverage}
+
+There are 6 function definitions that are not stubbed. They represent 50 statements, of which 50 are potentially reachable through EVA, resulting in a **statement coverage of 100.0%** with respect to the entire application.
+
+
+There were potentially 6 functions syntactically reachable from main.
+These functions contain 50 statements, of which 50 are potentially reachable according to EVA, resulting in a **statement coverage of 100.0%** with respect to the perimeter set by this entry point.
+
+
+# Warnings {#warnings}
+
+The table below lists the warning that have been emitted by the analyzer.
+They might put additional assumptions on the relevance
+of the analysis results and must be reviewed carefully
+
+Note that this does not take into account emitted alarms:
+they are reported in [the next section](#alarms)
+
+
+
+Table: Warning reported by Frama-C
+
+| Location | Description |
+|:---------|:------------|
+| tests/eva/cwe126.c:28 | `out of bounds read. assert \valid_read(data + i);` (emitted by `eva`) |
+
+
+## Warning 0 (tests/eva/cwe126.c:28) {#warn-0}
+
+Message:
+
+```
+[eva] out of bounds read. assert \valid_read(data + i);
+```
+
+
+
+# Results of the analysis {#alarms}
+
+The table below lists the alarm that have been emitted during the analysis.
+Any execution starting from `main`
+in a context matching the one used for the analysis
+will be immune from any other undefined behavior.
+More information on each individual alarm is
+given in the remainder of this section
+
+
+Table: Alarm emitted by the analysis
+
+| No | Kind | Emitter | Function | Location |
+|:---:|:----:|:-------:|:---------|:---------|
+| [0](#alarm-0) | `mem_access` | `Eva` | `CWE126_Buffer_Overread__malloc_char_loop_64b_badSink` | tests/eva/cwe126.c:28 |
+
+
+## Alarm 0 at tests/eva/cwe126.c:28 {#Alarm-0}
+
+The following ACSL assertion must hold to avoid invalid pointer dereferencing
+(undefined behavior).
+
+```acsl
+assert mem_access: \valid_read(data + i);
+```
+
+
+
+This alarm is real: Eva correctly identified the issue and did not report
+any spurious alarm anywhere else.
\ No newline at end of file
diff --git a/src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle b/src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f07744fc4323039b628e134ac97025b35e15c362
--- /dev/null
+++ b/src/plugins/markdown-report/tests/eva/oracle/cwe126.res.oracle
@@ -0,0 +1,57 @@
+[kernel] Parsing tests/eva/cwe126.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] tests/eva/cwe126.c:76: allocating variable __malloc_goodG2B_l76
+[eva] using specification for function exit
+[eva] FRAMAC_SHARE/libc/string.h:118:
+ cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
+[eva] tests/eva/cwe126.c:62: starting to merge loop iterations
+[eva] tests/eva/cwe126.c:40:
+ allocating variable __malloc_CWE126_Buffer_Overread__malloc_char_loop_64_bad_l40
+[eva] tests/eva/cwe126.c:26: starting to merge loop iterations
+[eva:alarm] tests/eva/cwe126.c:28: Warning:
+ out of bounds read. assert \valid_read(data + i);
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states]
+ Values at end of function CWE126_Buffer_Overread__malloc_char_loop_64b_badSink:
+ dataPtr ∈ {{ &data }}
+ data ∈ ESCAPINGADDR
+ data ∈ ESCAPINGADDR
+[eva:final-states]
+ Values at end of function CWE126_Buffer_Overread__malloc_char_loop_64_bad:
+ __fc_heap_status ∈ [--..--]
+ data ∈ ESCAPINGADDR
+[eva:final-states]
+ Values at end of function CWE126_Buffer_Overread__malloc_char_loop_64b_goodG2BSink:
+ dataPtr ∈ {{ &data }}
+ data ∈ ESCAPINGADDR
+ data ∈ ESCAPINGADDR
+[eva:final-states] Values at end of function goodG2B:
+ __fc_heap_status ∈ [--..--]
+ data ∈ ESCAPINGADDR
+[eva:final-states]
+ Values at end of function CWE126_Buffer_Overread__malloc_char_loop_64_good:
+ __fc_heap_status ∈ [--..--]
+[eva:final-states] Values at end of function main:
+ __fc_heap_status ∈ [--..--]
+ __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 6 functions analyzed (out of 6): 100% coverage.
+ In these functions, 54 statements reached (out of 54): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 invalid memory access
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 0 unknown 0 invalid 0 total
+ Preconditions 8 valid 0 unknown 0 invalid 8 total
+ 100% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
+[mdr] Report tests/eva/result/cwe126.0.md generated
diff --git a/src/plugins/markdown-report/tests/eva/test_config b/src/plugins/markdown-report/tests/eva/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..2d99fda9914fe40e3d6dad849ead724f9a88ec2e
--- /dev/null
+++ b/src/plugins/markdown-report/tests/eva/test_config
@@ -0,0 +1,2 @@
+CMD: @frama-c@ -eva @PTEST_FILE@ -mdr-gen md -mdr-date="now" -mdr-out @PTEST_DIR@/result/@PTEST_NAME@.@PTEST_NUMBER@.md
+LOG: @PTEST_NAME@.@PTEST_NUMBER@.md
diff --git a/src/plugins/server/data.ml b/src/plugins/server/data.ml
index 796f4c54dce76dfcd7a8422f0e45706c55c44694..961a30ae148b87dd286ddc6cb2f2672f622f4ba3 100644
--- a/src/plugins/server/data.ml
+++ b/src/plugins/server/data.ml
@@ -225,7 +225,7 @@ module Jtext =
struct
include Jany
let syntax = Syntax.publish ~page:text_page ~name:"text"
- ~synopsis:Syntax.any ~descr:(Markdown.rm "Formatted text.") ()
+ ~synopsis:Syntax.any ~descr:(Markdown.plain "Formatted text.") ()
end
(* -------------------------------------------------------------------------- *)
@@ -234,41 +234,66 @@ end
module Fmap = Map.Make(String)
-module Record( R : Info ) =
-struct
+type 'a record = json Fmap.t
- type t = json Fmap.t
+type ('r,'a) field = {
+ member : 'r record -> bool ;
+ getter : 'r record -> 'a ;
+ setter : 'r record -> 'a -> 'r record ;
+}
- type 'a field = {
- member : t -> bool ;
- getter : t -> 'a ;
- setter : t -> 'a -> t ;
- }
+type 'a signature = {
+ page : Doc.page ;
+ name : string ;
+ descr : Markdown.text ;
+ mutable fields : Syntax.field list ;
+ mutable default : 'a record ;
+ mutable published : bool ;
+}
- (* Declared Fields in this Record *)
- let fdocs = ref []
- let defaults = ref Fmap.empty
+module Record =
+struct
- let default () = !defaults
- let has fd r = fd.member r
- let get fd r = fd.getter r
- let set fd v r = fd.setter r v
+ module type S =
+ sig
+ type r
+ include S with type t = r record
+ val default : t
+ val has : (r,'a) field -> t -> bool
+ val get : (r,'a) field -> t -> 'a
+ val set : (r,'a) field -> 'a -> t -> t
+ end
+
+ let signature ~page ~name ~descr () = {
+ page ; name ; descr ;
+ published = false ;
+ fields = [] ;
+ default = Fmap.empty ;
+ }
- let field (type a) name ~descr ?default (d : a data) : a field =
+ let field (type a r) (s : r signature)
+ ~name ~descr ?default (d : a data) : (r,a) field =
+ if s.published then
+ raise (Invalid_argument "Server.Data.Record.field") ;
let module D = (val d) in
begin match default with
| None -> ()
- | Some v -> defaults := Fmap.add name (D.to_json v) !defaults
+ | Some v -> s.default <- Fmap.add name (D.to_json v) s.default
end ;
- fdocs := Syntax.{ name ; syntax = D.syntax ; descr } :: !fdocs ;
+ let field = Syntax.{ name ; syntax = D.syntax ; descr } in
+ s.fields <- field :: s.fields ;
let member r = Fmap.mem name r in
let getter r = D.of_json (Fmap.find name r) in
let setter r v = Fmap.add name (D.to_json v) r in
{ member ; getter ; setter }
- let option (type a) name ~descr (d : a data) : a option field =
+ let option (type a r) (s : r signature)
+ ~name ~descr (d : a data) : (r,a option) field =
+ if s.published then
+ raise (Invalid_argument "Server.Data.Record.option") ;
let module D = (val d) in
- fdocs := Syntax.{ name ; syntax = option D.syntax ; descr } :: !fdocs ;
+ let field = Syntax.{ name ; syntax = option D.syntax ; descr } in
+ s.fields <- field :: s.fields ;
let member r = Fmap.mem name r in
let getter r =
try Some (D.of_json (Fmap.find name r)) with Not_found -> None in
@@ -277,21 +302,36 @@ struct
| Some v -> Fmap.add name (D.to_json v) r in
{ member ; getter ; setter }
- let fields () = Syntax.fields ~title:"Field" !fdocs
-
- let syntax =
- Syntax.publish ~page:R.page ~name:R.name
- ~descr:R.descr
- ~synopsis:(Syntax.record [])
- ~details:(Markdown.mk_block fields) ()
-
- let of_json js =
- List.fold_left
- (fun r (fd,js) -> Fmap.add fd js r)
- (default ()) (Ju.to_assoc js)
-
- let to_json r : json =
- `Assoc (Fmap.fold (fun fd js fds -> (fd,js) :: fds) r [])
+ let publish (type r) (s : r signature) =
+ if s.published then
+ raise (Invalid_argument "Server.Data.Record.publish") ;
+ let module M =
+ struct
+ type nonrec r = r
+ type t = r record
+ let descr = s.descr
+ let syntax =
+ let fields = Syntax.fields ~title:"Field" (List.rev s.fields) in
+ Syntax.publish ~page:s.page ~name:s.name ~descr
+ ~synopsis:(Syntax.record [])
+ ~details:[fields] ()
+ let default = s.default
+ let has fd r = fd.member r
+ let get fd r = fd.getter r
+ let set fd v r = fd.setter r v
+ let of_json js =
+ List.fold_left
+ (fun r (fd,js) -> Fmap.add fd js r)
+ default (Ju.to_assoc js)
+ let to_json r : json =
+ `Assoc (Fmap.fold (fun fd js fds -> (fd,js) :: fds) r [])
+ end in
+ begin
+ s.default <- Fmap.empty ;
+ s.fields <- [] ;
+ s.published <- true ;
+ (module M : S with type r = r)
+ end
end
@@ -507,13 +547,16 @@ struct
) E.values
end
- let values () =
- Markdown.table
- [ `Left E.name ; `Left "Description" ]
- (List.map
- (fun (_,tag,descr) ->
- [ Markdown.tt (Printf.sprintf "%S" tag) ; descr ]
- ) E.values)
+ let values =
+ let open Markdown in
+ let caption = Some (plain "Values description") in
+ let header = [ plain E.name, Left; plain "Description", Left ] in
+ let content =
+ List.map
+ (fun (_,tag,descr) -> [ format "`%S`" tag ; descr ])
+ E.values
+ in
+ Table { caption; header; content }
include Collection
(struct
@@ -522,7 +565,7 @@ struct
let syntax = Syntax.publish
~page:E.page ~name:E.name
~synopsis:Syntax.ident
- ~descr:E.descr ~details:(Markdown.mk_block values) ()
+ ~descr:E.descr ~details:[values] ()
let to_json value =
register () ;
diff --git a/src/plugins/server/data.mli b/src/plugins/server/data.mli
index 3e10ece5cbfb35d8753129d85d094c118919bab0..52ab09382893efb8fa7d8c3907197bd9affc707f 100644
--- a/src/plugins/server/data.mli
+++ b/src/plugins/server/data.mli
@@ -94,33 +94,62 @@ module Jtext : S with type t = json (** Rich text encoding, see [Jbuffer] *)
(** {2 Records} *)
(* -------------------------------------------------------------------------- *)
-module Record(R : Info) :
+type 'a record (** Records of type 'a *)
+type 'a signature (** Opened signature for record of type ['a] *)
+type ('a,'b) field (** Field of type ['b] for a record of type ['a] *)
+
+(** Record factory.
+
+ You shall start by declaring a (ghost) type [r] and call
+ [Record.signature] to create a signature of type [r].
+ Then, populate the record with [Record.field] or [Record.option].
+ Finally, you shall call [Record.publish] to obtain a new data module
+ of type [Record with type r = r], which gives you a [Data] with an opaque
+ type [t = r record] with fields of type [(r,a) field].
+
+ {[
+ (* ---- Exemple of Record Data --- *)
+ type r
+ let s = Record.signature ~page ~kind ~name ~descr () in
+ let fd_a = Record.field s ~name:"a" ~descr:"..." (module A) in
+ let fd_b = Record.field s ~name:"b" ~descr:"..." (module B) in
+
+ module M = (val (Record.publish s) : Record with type r = r)
+
+ let make a b = M.default |> M.set fd_a a |> M.set fd_b b
+ ]}
+*)
+module Record :
sig
- (** A new type [t] is created for each application of the functor. *)
- include S
-
- (** Parametric field. Can only be used with type [t]. *)
- type 'a field
-
- (** Field constructor *)
- val field : string -> descr:Markdown.text -> ?default:'a -> 'a data -> 'a field
-
- (** Optional field constructor *)
- val option : string -> descr:Markdown.text -> 'a data -> 'a option field
-
- (** Field presence. If the field has a default value, it will be always
- present. *)
- val has : 'a field -> t -> bool
-
- (** Field accessor.
- @raise Not_found if the field is optional and not present *)
- val get : 'a field -> t -> 'a
-
- (** Field updator. *)
- val set : 'a field -> 'a -> t -> t
- (** Contains only the default values. *)
- val default : unit -> t
+ (** Data with [type t = r record].
+ Also contains getters and setters for fields. *)
+ module type S =
+ sig
+ type r
+ include S with type t = r record
+ val default : t
+ val has : (r,'a) field -> t -> bool
+ val get : (r,'a) field -> t -> 'a
+ val set : (r,'a) field -> 'a -> t -> t
+ end
+
+ (** Create a new, opened record type *)
+ val signature : page:Doc.page -> name:string -> descr:Markdown.text ->
+ unit -> 'a signature
+
+ (** Adds a field to an opened record *)
+ val field : 'r signature ->
+ name:string -> descr:Markdown.text -> ?default:'a -> 'a data ->
+ ('r,'a) field
+
+ (** Adds a optional field to an opened record *)
+ val option : 'r signature ->
+ name:string -> descr:Markdown.text -> 'a data ->
+ ('r,'a option) field
+
+ (** Publish and close an opened record *)
+ val publish : 'a signature -> (module S with type r = 'a)
end
diff --git a/src/plugins/server/doc.ml b/src/plugins/server/doc.ml
index 0d141b3f018ecdd7b1946c5fa5f0db5a76bfd16f..c54ec9e8a912285da1f573fbdfc4c76e651ab91c 100644
--- a/src/plugins/server/doc.ml
+++ b/src/plugins/server/doc.ml
@@ -24,6 +24,7 @@
(* --- Server Documentation --- *)
(* -------------------------------------------------------------------------- *)
+open Markdown
type json = Yojson.Basic.t
module Senv = Server_parameters
module Pages = Map.Make(String)
@@ -36,8 +37,8 @@ type page = {
chapter : chapter ;
title : string ;
order : int ;
- intro : Markdown.section ;
- mutable sections : Markdown.section list ;
+ intro : Markdown.elements ;
+ mutable sections : Markdown.elements list ;
}
let order = ref 0
@@ -45,7 +46,7 @@ let pages : page Pages.t ref = ref Pages.empty
let plugins : string list ref = ref []
let entries : (string * Markdown.href) list ref = ref []
let path page = page.path
-let href page name : Markdown.href = `Section( page.path , name )
+let href page name : Markdown.href = Section( page.path , name )
(* -------------------------------------------------------------------------- *)
(* --- Page Collection --- *)
@@ -73,8 +74,8 @@ let page chapter ~title ~filename =
Printf.sprintf "%s/%s/server/%s" Config.datadir name filename in
let intro =
if Sys.file_exists intro
- then Markdown.read_section intro
- else Markdown.(section ~title empty []) in
+ then Markdown.rawfile intro
+ else Markdown.(section ~title []) in
let order = incr order ; !order in
let page = { order ; rootdir ; path ;
chapter ; title ; intro ;
@@ -83,8 +84,8 @@ let page chapter ~title ~filename =
let publish ~page ?name ?(index=[]) ~title content sections =
let id = match name with Some id -> id | None -> title in
- let href = `Section( page.path , id ) in
- let section = Markdown.section ?name ~title content sections in
+ let href = Section( page.path , id ) in
+ let section = Markdown.section ?name ~title (content @ sections) in
List.iter (fun entry -> entries := (entry , href) :: !entries) index ;
page.sections <- section :: page.sections ; href
@@ -105,27 +106,23 @@ let pages_of_chapter c =
(fun _ p -> if p.chapter = c then w := p :: !w) !pages ;
List.sort (fun p q -> p.order - q.order) !w
-let table_of_chapter c fmt =
- begin
- Format.fprintf fmt "## %s@\n@." (title_of_chapter c) ;
- List.iter
- (fun p -> Format.fprintf fmt " - [%s](%s)@." p.title p.path)
- (pages_of_chapter c) ;
- Format.pp_print_newline fmt () ;
- end
+let table_of_chapter c =
+ [H2 (Markdown.plain (title_of_chapter c), None);
+ Block (list (List.map
+ (fun p -> text (link ~text:(plain p.title) ~page:p.path ()))
+ (pages_of_chapter c)))]
-let table_of_contents fmt =
- begin
- table_of_chapter `Protocol fmt ;
- table_of_chapter `Kernel fmt ;
- List.iter
- (fun p -> table_of_chapter (`Plugin p) fmt)
- (List.sort String.compare !plugins)
- end
+let table_of_contents () =
+ table_of_chapter `Protocol @
+ table_of_chapter `Kernel @
+ List.concat
+ (List.map
+ (fun p -> table_of_chapter (`Plugin p))
+ (List.sort String.compare !plugins))
let index () =
List.map
- (fun (title,entry) -> Markdown.href ~title entry)
+ (fun (title,entry) -> Markdown.href ~text:(plain title) entry)
(List.sort (fun (a,_) (b,_) -> String.compare a b) !entries)
let link ~toc ~title ~href : json =
@@ -162,13 +159,26 @@ let metadata page : json =
(* --- Dump Documentation --- *)
(* -------------------------------------------------------------------------- *)
+let pp_one_page ~root ~page ~title body =
+ let full_path = Filepath.normalize (root ^ "/" ^ page) in
+ let dir = Filename.dirname full_path in
+ if not (Sys.file_exists dir) then Extlib.mkdir ~parents:true dir 0o755;
+ try
+ let chan = open_out full_path in
+ let fmt = Format.formatter_of_out_channel chan in
+ let title = plain title in
+ Markdown.(pp_pandoc ~page fmt (pandoc ~title body))
+ with Sys_error e ->
+ Senv.fatal "Could not open file %s for writing: %s" full_path e
+
let dump ~root ?(meta=true) () =
begin
Pages.iter
(fun path page ->
Senv.feedback "[doc] Page: '%s'" path ;
let body = Markdown.subsections page.intro (List.rev page.sections) in
- Markdown.dump ~root ~page:path (Markdown.document body) ;
+ let title = page.title in
+ pp_one_page ~root ~page:path ~title body ;
if meta then
let path = Printf.sprintf "%s/%s.json" root path in
Yojson.Basic.to_file path (metadata page) ;
@@ -177,14 +187,17 @@ let dump ~root ?(meta=true) () =
if meta then
let path = Printf.sprintf "%s/readme.md.json" root in
Yojson.Basic.to_file path maindata ;
- Markdown.(dump ~root ~page:"readme.md"
- begin
- h1 "Documentation" </>
- par (bf "Version" <+> rm Config.version) </>
- fmt_block table_of_contents </>
- h2 "Index" </>
- list (index ())
- end) ;
+ let body =
+ [ H1 (plain "Documentation", None);
+ Block (text (format "Version %s" Config.version))]
+ @
+ table_of_contents ()
+ @
+ [H2 (plain "Index", None);
+ Block (list (List.map text (index ())))]
+ in
+ let title = "Documentation" in
+ pp_one_page ~root ~page:"readme.md" ~title body
end
let () =
diff --git a/src/plugins/server/doc.mli b/src/plugins/server/doc.mli
index e204916f44b8eec01dcc173221c77821bc990e9b..e80db0a9a2ad8241af9a9acb867a207e95a9227f 100644
--- a/src/plugins/server/doc.mli
+++ b/src/plugins/server/doc.mli
@@ -56,9 +56,9 @@ val publish :
?name:string ->
?index:string list ->
title:string ->
- Markdown.block ->
- Markdown.section list ->
- href
+ Markdown.elements ->
+ Markdown.elements ->
+ Markdown.href
(** Dumps all published pages of documentations. Unless [~meta:false],
also generates METADATA for each page in
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 77605bf53f37fa4b3c2518de252644bcaa148c17..9001f346b63aadfbbae5e11d7ceb160f87679c0c 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -35,7 +35,7 @@ let page = Doc.page `Kernel ~title:"Ast Services" ~filename:"ast.md"
let () = Request.register ~page
~kind:`EXEC ~name:"kernel.ast.compute"
- ~descr:(Md.rm "Ensures that AST is computed")
+ ~descr:(Md.plain "Ensures that AST is computed")
~input:(module Junit) ~output:(module Junit) Ast.compute
(* -------------------------------------------------------------------------- *)
@@ -104,7 +104,7 @@ module Stmt = Data.Collection
type t = stmt
let syntax = Sy.publish ~page ~name:"stmt"
~synopsis:Sy.ident
- ~descr:(Md.rm "Code statement identifier") ()
+ ~descr:(Md.plain "Code statement identifier") ()
let to_json st = `String (Tag.of_stmt st)
let of_json js =
let id = Js.to_string js in
@@ -134,7 +134,7 @@ module Kf = Data.Collection
type t = kernel_function
let syntax = Sy.publish ~page ~name:"fct-id"
~synopsis:Sy.ident
- ~descr:(Md.rm "Function identified by its global name.") ()
+ ~descr:(Md.plain "Function identified by its global name.") ()
let to_json kf =
`String (Kernel_function.get_name kf)
let of_json js =
@@ -149,7 +149,7 @@ module Kf = Data.Collection
let () = Request.register ~page
~kind:`GET ~name:"kernel.ast.getFunctions"
- ~descr:(Md.rm "Collect all functions in the AST")
+ ~descr:(Md.plain "Collect all functions in the AST")
~input:(module Junit) ~output:(module Kf.Jlist)
begin fun () ->
let pool = ref [] in
@@ -159,7 +159,7 @@ let () = Request.register ~page
let () = Request.register ~page
~kind:`GET ~name:"kernel.ast.printFunction"
- ~descr:(Md.rm "Print the AST of a function")
+ ~descr:(Md.plain "Print the AST of a function")
~input:(module Kf) ~output:(module Jtext)
(fun kf -> Jbuffer.to_json PP.pp_global (Kernel_function.get_global kf))
diff --git a/src/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml
index 7448c53e42df57194b8c9855689822507fb1e25a..49e11148a95a714eb77d28b4a947e56774c34fca 100644
--- a/src/plugins/server/kernel_main.ml
+++ b/src/plugins/server/kernel_main.ml
@@ -38,15 +38,15 @@ let page = Doc.page `Kernel ~title:"Kernel Services" ~filename:"kernel.md"
let () =
let get_config = Request.signature
~page ~kind:`GET ~name:"kernel.getConfig"
- ~descr:(Md.rm "Frama-C Kernel configuration")
+ ~descr:(Md.plain "Frama-C Kernel configuration")
~input:(module Junit) () in
let result name descr =
- Request.result get_config ~name ~descr:(Md.rm descr) (module Jstring) in
+ Request.result get_config ~name ~descr:(Md.plain descr) (module Jstring) in
let set_version = result "version" "Frama-C version" in
let set_datadir = result "datadir" "Shared directory (FRAMAC_SHARE)" in
let set_libdir = result "libdir" "Lib directory (FRAMAC_LIB)" in
let set_pluginpath = Request.result get_config
- ~name:"pluginpath" ~descr:(Md.rm "Plugin directories (FRAMAC_PLUGIN)")
+ ~name:"pluginpath" ~descr:(Md.plain "Plugin directories (FRAMAC_PLUGIN)")
(module Jstring.Jlist) in
Request.register_sig get_config
begin fun rq () ->
@@ -63,11 +63,13 @@ let () =
module RawSource =
struct
type t = Filepath.position
+
let syntax = Sy.publish ~page ~name:"source"
~synopsis:(Sy.record [ "file" , Sy.string ; "line" , Sy.int ])
- ~descr:(Md.rm "Source file positions.")
- ~details:(Md.praw "The file path is normalized, \
- and the line number starts at one.") ()
+ ~descr:(Md.plain "Source file positions.")
+ ~details:Md.([Block [Text (plain "The file path is normalized, \
+ and the line number starts at one.")]])
+ ()
let to_json p = `Assoc [
"file" , `String (p.Filepath.pos_path :> string) ;
@@ -93,14 +95,14 @@ struct
type t = Log.kind
let page = page
let name = "kind"
- let descr = Md.rm "Frama-C message category."
+ let descr = Md.plain "Frama-C message category."
let values = [
- Log.Error, "ERROR", Md.rm "User Error" ;
- Log.Warning, "WARNING", Md.rm "User Warning" ;
- Log.Feedback, "FEEDBACK", Md.rm "Analyzer Feedback" ;
- Log.Result, "RESULT", Md.rm "Analyzer Result" ;
- Log.Failure, "FAILURE", Md.rm "Analyzer Failure" ;
- Log.Debug, "DEBUG", Md.rm "Analyser Debug" ;
+ Log.Error, "ERROR", Md.plain "User Error" ;
+ Log.Warning, "WARNING", Md.plain "User Warning" ;
+ Log.Feedback, "FEEDBACK", Md.plain "Analyzer Feedback" ;
+ Log.Result, "RESULT", Md.plain "Analyzer Result" ;
+ Log.Failure, "FAILURE", Md.plain "Analyzer Failure" ;
+ Log.Debug, "DEBUG", Md.plain "Analyser Debug" ;
]
end
@@ -113,31 +115,29 @@ module LogKind = Dictionary(RawKind)
module RawEvent =
struct
- module R = Record
- (struct
- let page = page
- let name = "log"
- let descr = Md.rm "Message event record."
- end)
-
- let syntax = R.syntax
+ type rlog
- let descr = Md.rm
- let kind = R.field "kind" ~descr:(descr "Message kind") (module LogKind)
- let plugin = R.field "plugin" ~descr:(descr "Emitter plugin") (module Jstring)
- let message = R.field "message" ~descr:(descr "Message text") (module Jstring)
+ let jlog : rlog signature = Record.signature ~page
+ ~name:"log" ~descr:(Md.plain "Message event record.") ()
- let category = R.option "category"
- ~descr:(descr "Message category (DEBUG or WARNING)")
- (module Jstring)
+ let kind = Record.field jlog ~name:"kind"
+ ~descr:(Md.plain "Message kind") (module LogKind)
+ let plugin = Record.field jlog ~name:"plugin"
+ ~descr:(Md.plain "Emitter plugin") (module Jstring)
+ let message = Record.field jlog ~name:"message"
+ ~descr:(Md.plain "Message text") (module Jstring)
+ let category = Record.option jlog ~name:"category"
+ ~descr:(Md.plain "Message category (DEBUG or WARNING)") (module Jstring)
+ let source = Record.option jlog ~name:"source"
+ ~descr:(Md.plain "Source file position") (module LogSource)
- let source = R.option "source" ~descr:(descr "Source file position")
- (module LogSource)
+ module R = (val (Record.publish jlog) : Record.S with type r = rlog)
type t = Log.event
+ let syntax = R.syntax
let to_json evt =
- R.default () |>
+ R.default |>
R.set plugin evt.Log.evt_plugin |>
R.set kind evt.Log.evt_kind |>
R.set category evt.Log.evt_category |>
@@ -195,12 +195,12 @@ let () =
let () = Request.register
~page ~kind:`SET ~name:"kernel.setLogs"
- ~descr:(Md.rm "Turn logs monitoring on/off")
+ ~descr:(Md.plain "Turn logs monitoring on/off")
~input:(module Jbool) ~output:(module Junit) monitor
let () = Request.register
~page ~kind:`GET ~name:"kernel.getLogs"
- ~descr:(Md.rm "Flush the last emitted logs since last call (max 100)")
+ ~descr:(Md.plain "Flush the last emitted logs since last call (max 100)")
~input:(module Junit) ~output:(module LogEvent.Jlist)
begin fun () ->
let pool = ref [] in
diff --git a/src/plugins/server/kernel_project.ml b/src/plugins/server/kernel_project.ml
index 883cea34f37b7ec3b8725d2c62282b14c07d22d9..f2fd2ec4d9e7a72e6e98f90f593fb6d5991f804d 100644
--- a/src/plugins/server/kernel_project.ml
+++ b/src/plugins/server/kernel_project.ml
@@ -37,7 +37,7 @@ module ProjectInfo =
type t = Project.t
let syntax = Sy.publish ~page ~name:"project-info"
- ~descr:(Md.rm "Project informations")
+ ~descr:(Md.plain "Project informations")
~synopsis:Sy.(record[ "id",ident; "name",string; "current",boolean ])
()
@@ -63,7 +63,7 @@ struct
let syntax = Sy.publish ~page ~name:"project-request"
~synopsis:(Sy.(record[ "project",ident; "request",string; "data",any; ]))
- ~descr:(Md.rm "Request to be executed on the specified project.") ()
+ ~descr:(Md.plain "Request to be executed on the specified project.") ()
let of_json js =
begin
@@ -86,37 +86,37 @@ end
let () = Request.register ~page
~kind:`GET ~name:"kernel.project.getCurrent"
- ~descr:(Md.rm "Returns the current project")
+ ~descr:(Md.plain "Returns the current project")
~input:(module Junit) ~output:(module ProjectInfo)
Project.current
let () = Request.register ~page
~kind:`SET ~name:"kernel.project.setCurrent"
- ~descr:(Md.rm "Switches the current project")
+ ~descr:(Md.plain "Switches the current project")
~input:(module Jident) ~output:(module Junit)
(fun pid -> Project.(set_current (from_unique_name pid)))
let () = Request.register ~page
~kind:`GET ~name:"kernel.project.getList"
- ~descr:(Md.rm "Returns the list of all projects")
+ ~descr:(Md.plain "Returns the list of all projects")
~input:(module Junit) ~output:(module ProjectInfo.Jlist)
(fun () -> Project.fold_on_projects (fun ids p -> p :: ids) [])
let () = Request.register ~page
~kind:`GET ~name:"kernel.project.getOn"
- ~descr:(Md.rm "Execute a GET request within the given project")
+ ~descr:(Md.plain "Execute a GET request within the given project")
~input:(module ProjectRequest) ~output:(module Jany)
(ProjectRequest.process `GET)
let () = Request.register ~page
~kind:`SET ~name:"kernel.project.setOn"
- ~descr:(Md.rm "Execute a SET request within the given project")
+ ~descr:(Md.plain "Execute a SET request within the given project")
~input:(module ProjectRequest) ~output:(module Jany)
(ProjectRequest.process `SET)
let () = Request.register ~page
~kind:`EXEC ~name:"kernel.project.execOn"
- ~descr:(Md.rm "Execute an EXEC request within the given project")
+ ~descr:(Md.plain "Execute an EXEC request within the given project")
~input:(module ProjectRequest) ~output:(module Jany)
(ProjectRequest.process `EXEC)
diff --git a/src/plugins/server/request.ml b/src/plugins/server/request.ml
index 039ee9f3c3c161cc5fb5d7f9fa688b1f50b625ec..01fd23fe22225c248c14dad8b62b96be6102b73f 100644
--- a/src/plugins/server/request.ml
+++ b/src/plugins/server/request.ml
@@ -144,18 +144,18 @@ let sy_output (type b) (output : b rq_output) : Syntax.t =
| Rfields _ -> Syntax.record []
(* json input documentation *)
-let doc_input (type a) (input : a rq_input) : Markdown.block =
+let doc_input (type a) (input : a rq_input) =
match input with
| Pnone -> assert false
- | Pdata _ -> Markdown.empty
- | Pfields fs -> Syntax.fields ~title:"Input" (List.rev fs)
+ | Pdata _ -> []
+ | Pfields fs -> [Syntax.fields ~title:"Input" (List.rev fs)]
(* json output syntax *)
-let doc_output (type b) (output : b rq_output) : Markdown.block =
+let doc_output (type b) (output : b rq_output) =
match output with
| Rnone -> assert false
- | Rdata _ -> Markdown.empty
- | Rfields fs -> Syntax.fields ~title:"Output" (List.rev fs)
+ | Rdata _ -> []
+ | Rfields fs -> [Syntax.fields ~title:"Output" (List.rev fs)]
(* -------------------------------------------------------------------------- *)
(* --- Multi-Parameters Requests --- *)
@@ -253,8 +253,7 @@ let result_opt (type a b) (s : (a,unit) signature) ~name ~descr
(* -------------------------------------------------------------------------- *)
let signature
- ~page ~kind ~name ~descr ?(details=Markdown.empty)
- ?input ?output () =
+ ~page ~kind ~name ~descr ?(details=[]) ?input ?output () =
check_name name ;
check_page page name ;
check_kind kind name ;
@@ -299,6 +298,7 @@ let mk_output (type b) name required (output : b rq_output) : (rq -> b -> json)
fmap_to_json rq.result)
let register_sig (type a b) (s : (a,b) signature) (process : rq -> a -> b) =
+ let open Markdown in
if s.defined then
Senv.fatal "Request '%s' is defined twice" s.name ;
let input = mk_input s.name s.defaults s.input in
@@ -309,20 +309,18 @@ let register_sig (type a b) (s : (a,b) signature) (process : rq -> a -> b) =
in
let skind = Main.string_of_kind s.kind in
let title = Printf.sprintf "`%s` %s" skind s.name in
- let synopsis =
- Markdown.table
- [`Center "Input" ; `Center "Output" ]
- [[ Syntax.format @@ sy_input s.input ;
- Syntax.format @@ sy_output s.output ]] in
+ let header = [ plain "Input", Center; plain "Output", Center] in
let content =
- Markdown.concat [
- Markdown.par s.descr ;
- synopsis ;
- s.details ;
- doc_input s.input ;
- doc_output s.output ;
- ] in
- let _ = Doc.publish ~page:s.page ~name:s.name ~title content [] in
+ [[ Syntax.text @@ sy_input s.input ;
+ Syntax.text @@ sy_output s.output ]]
+ in
+ let synopsis = Table { caption=None ; header; content } in
+ let description =
+ [ Block [Text s.descr ] ; synopsis ; Block s.details] @
+ doc_input s.input @
+ doc_output s.output
+ in
+ let _ = Doc.publish ~page:s.page ~name:s.name ~title description [] in
Main.register s.kind s.name processor ;
s.defined <- true
diff --git a/src/plugins/server/syntax.ml b/src/plugins/server/syntax.ml
index 565a227cde54a50190a518e5d45f036b9b44d913..41d2b8e45ff7f87c49d5a57afaeba5f623be4da6 100644
--- a/src/plugins/server/syntax.ml
+++ b/src/plugins/server/syntax.ml
@@ -55,58 +55,57 @@ type t = { atomic:bool ; text:Markdown.text }
let atom md = { atomic=true ; text=md }
let flow md = { atomic=false ; text=md }
+let text { text } = text
-let format { text } = text
let protect a =
- if a.atomic then a.text else Markdown.(rm "(" <+> a.text <+> rm ")")
+ if a.atomic then a.text else Markdown.(plain "(" @ a.text @ plain ")")
-let publish ~page ~name ~descr ~synopsis ?(details = Markdown.empty) () =
+let publish ~page ~name ~descr ~synopsis ?(details = []) () =
check_name name ;
check_page page name ;
let id = Printf.sprintf "data-%s" name in
let title = Printf.sprintf "`DATA` %s" name in
- let format = ref Markdown.nil in
- let syntax = Markdown.fmt_block (fun fmt ->
- Format.fprintf fmt "> %a ::= %a"
- Markdown.pp_text !format
- Markdown.pp_text synopsis.text
- ) in
- let content = Markdown.( par descr </> syntax </> details ) in
- let href = Doc.publish ~page ~name:id ~title ~index:[name] content [] in
- let link_title = Printf.sprintf "_%s_" name in
- let link = Markdown.href ~title:link_title href in
- format := link ; atom @@ link
-
-let unit = atom @@ Markdown.rm "-"
-let any = atom @@ Markdown.it "any"
-let int = atom @@ Markdown.it "int"
-let ident = atom @@ Markdown.it "ident"
-let string = atom @@ Markdown.it "string"
-let number = atom @@ Markdown.it "number"
-let boolean = atom @@ Markdown.it "boolean"
-
-let escaped name = Markdown.tt @@ Printf.sprintf "'%s'" @@ String.escaped name
+ let dref = Doc.href page id in
+ let dlink = Markdown.href ~text:(Markdown.emph name) dref in
+ let syntax = Markdown.(glue [
+ plain "<" ; dlink ; plain ">" ; plain ":=" ; synopsis.text ]) in
+ let content = Markdown.(Block ( text descr @ text syntax ) :: details) in
+ let _href = Doc.publish ~page ~name:id ~title ~index:[name] content [] in
+ atom dlink
+
+let unit = atom @@ Markdown.plain "-"
+let any = atom @@ Markdown.emph "any"
+let int = atom @@ Markdown.emph "int"
+let ident = atom @@ Markdown.emph "ident"
+let string = atom @@ Markdown.emph "string"
+let number = atom @@ Markdown.emph "number"
+let boolean = atom @@ Markdown.emph "boolean"
+
+let escaped name =
+ Markdown.code (Printf.sprintf "'%s'" @@ String.escaped name)
let tag name = atom @@ escaped name
-
-let array a = atom @@ Markdown.(tt "[" <+> protect a <+> tt ", … ]")
+let array a = atom @@ Markdown.(code "[" @ protect a @ code ", … ]")
let tuple ts =
- atom @@ Markdown.(tt "["
- <+> glue ~sep:(raw " `,` ") (List.map protect ts) <+>
- tt "]")
+ atom @@
+ Markdown.(
+ code "[" @
+ glue ~sep:(code ",") (List.map protect ts) @
+ code "]"
+ )
-let union ts = flow @@ Markdown.(glue ~sep:(raw " | ") (List.map protect ts))
+let union ts = flow @@ Markdown.(glue ~sep:(plain "|") (List.map protect ts))
-let option t = atom @@ Markdown.(protect t <@> tt "?")
+let option t = atom @@ Markdown.(protect t @ code "?")
-let field (a,t) = Markdown.( escaped a <+> tt ":" <+> t.text )
+let field (a,t) = Markdown.( escaped a @ code ":" @ t.text )
let record fds =
let fields =
- if fds = [] then Markdown.rm "…" else
- Markdown.(glue ~sep:(raw " `;` ") (List.map field fds))
- in atom @@ Markdown.(tt "{" <+> fields <+> tt "}")
+ if fds = [] then Markdown.plain "…" else
+ Markdown.(glue ~sep:(code ";") (List.map field fds))
+ in atom @@ Markdown.(code "{" @ fields @ code "}")
type field = {
name : string ;
@@ -115,15 +114,15 @@ type field = {
}
let fields ~title (fds : field list) =
- let c_field = `Left title in
- let c_format = `Center "Format" in
- let c_descr = `Left "Description" in
- Markdown.table [ c_field ; c_format ; c_descr ]
- begin
- List.map
- (fun f ->
- [ Markdown.tt f.name ; format f.syntax ; f.descr ])
- fds
- end
+ let open Markdown in
+ let header = [
+ plain title, Left;
+ plain "Format", Center;
+ plain "Description", Left
+ ] in
+ let column f = [ code f.name ; f.syntax.text ; f.descr ] in
+ Markdown.Table {
+ caption = None ; header ; content = List.map column fds ;
+ }
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/syntax.mli b/src/plugins/server/syntax.mli
index ff4c575e6c3ed0e65a38b66f593272850942ddaf..33ae244e8f3bea0b3bae9e34afd5ac67bf703852 100644
--- a/src/plugins/server/syntax.mli
+++ b/src/plugins/server/syntax.mli
@@ -26,14 +26,14 @@
type t
-val format : t -> Markdown.text
+val text : t -> Markdown.text
(** The provided synopsis must be very short, to fit in one line.
Extended definition, like record fields and such, must be detailed in
the description block. *)
val publish :
page:Doc.page -> name:string -> descr:Markdown.text ->
- synopsis:t -> ?details:Markdown.block -> unit -> t
+ synopsis:t -> ?details:Markdown.elements -> unit -> t
val unit : t
val any : t
@@ -54,6 +54,6 @@ type field = { name : string ; syntax : t ; descr : Markdown.text }
(** Builds a table with fields column named with [~title]
(shall be capitalized) *)
-val fields : title:string -> field list -> Markdown.block
+val fields : title:string -> field list -> Markdown.element
(* -------------------------------------------------------------------------- *)