package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file parse_remarks.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    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 %a"
    Filepath.Normalized.pretty f;
  try
    let chan = open_in (f:>string) in
    let { remarks } = parse_remarks (empty_env ()) chan in
    remarks
  with Sys_error err ->
    Mdr_params.error
      "Unable to open remarks file %a (%s). \
       No additional remarks will be included in the report."
      Filepath.Normalized.pretty f err;
    Datatype.String.Map.empty
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct