package frama-c

  1. Overview
  2. Docs

doc/src/frama-c.gui/cilconfig.ml.html

Source file cilconfig.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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
(***************************************************************************)
(*                                                                         *)
(*  SPDX-License-Identifier BSD-3-Clause                                   *)
(*  Copyright (C) 2001-2003                                                *)
(*  George C. Necula    <necula@cs.berkeley.edu>                           *)
(*  Scott McPeak        <smcpeak@cs.berkeley.edu>                          *)
(*  Wes Weimer          <weimer@cs.berkeley.edu>                           *)
(*  Ben Liblit          <liblit@cs.berkeley.edu>                           *)
(*  All rights reserved.                                                   *)
(*  File modified by                                                       *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)   *)
(*  INRIA (Institut National de Recherche en Informatique et Automatique)  *)
(*                                                                         *)
(***************************************************************************)

module H = Hashtbl


(************************************************************************

   Configuration

 ************************************************************************)

(** The configuration data can be of several types **)
type configData =
    ConfInt of int
  | ConfBool of bool
  | ConfFloat of float
  | ConfString of string
  | ConfList of configData list


(* Store here window configuration file *)
let configurationData: (string, configData) H.t = H.create 13

let clearConfiguration () = H.clear configurationData

let setConfiguration (key: string) (c: configData) =
  H.replace configurationData key c

let findConfiguration (key: string) : configData =
  H.find configurationData key

let findConfigurationInt (key: string) : int =
  match findConfiguration key with
    ConfInt i -> i
  | _ ->
    Kernel.warning "Configuration %s is not an integer" key;
    raise Not_found

let findConfigurationFloat (key: string) : float =
  match findConfiguration key with
    ConfFloat i -> i
  | _ ->
    Kernel.warning "Configuration %s is not a float" key;
    raise Not_found

let useConfigurationInt (key: string) (f: int -> unit) =
  try f (findConfigurationInt key)
  with Not_found -> ()

let useConfigurationFloat (key: string) (f: float -> unit) =
  try f (findConfigurationFloat key)
  with Not_found -> ()

let findConfigurationString (key: string) : string =
  match findConfiguration key with
    ConfString s -> s
  | _ ->
    Kernel.warning "Configuration %s is not a string" key;
    raise Not_found

let useConfigurationString (key: string) (f: string -> unit) =
  try f (findConfigurationString key)
  with Not_found -> ()


let findConfigurationBool (key: string) : bool =
  match findConfiguration key with
    ConfBool b -> b
  | _ ->
    Kernel.warning "Configuration %s is not a boolean" key;
    raise Not_found

let useConfigurationBool (key: string) (f: bool -> unit) =
  try f (findConfigurationBool key)
  with Not_found -> ()

let findConfigurationList (key: string) : configData list  =
  match findConfiguration key with
    ConfList l -> l
  | _ ->
    Kernel.warning "Configuration %s is not a list" key;
    raise Not_found

let useConfigurationList (key: string) (f: configData list -> unit) =
  try f (findConfigurationList key)
  with Not_found -> ()


let saveConfiguration (fname : Filepath.t) =
  (* Convert configuration data to a string, for saving externally *)
  let configToString (c: configData) : string =
    let buff = Buffer.create 80 in
    let rec loop (c: configData) : unit =
      match c with
        ConfInt i ->
        Buffer.add_char buff 'i';
        Buffer.add_string buff (string_of_int i);
        Buffer.add_char buff ';'

      | ConfBool b ->
        Buffer.add_char buff 'b';
        Buffer.add_string buff (string_of_bool b);
        Buffer.add_char buff ';'

      | ConfFloat f ->
        Buffer.add_char buff 'f';
        Buffer.add_string buff (string_of_float f);
        Buffer.add_char buff ';'

      | ConfString s ->
        if String.contains s '"' then
          Kernel.fatal "Guilib: configuration string contains quotes";
        Buffer.add_char buff '"';
        Buffer.add_string buff s;
        Buffer.add_char buff '"'; (* '"' *)

      | ConfList l ->
        Buffer.add_char buff '[';
        List.iter loop l;
        Buffer.add_char buff ']'
    in
    loop c;
    Buffer.contents buff
  in
  try
    let open Filesystem.Operators in
    let$ oc = Filesystem.with_open_out_exn fname in
    Kernel.debug "Saving configuration to %a@." Filepath.pretty_abs fname;
    H.iter (fun k c ->
        output_string oc (k ^ "\n");
        output_string oc ((configToString c) ^ "\n"))
      configurationData
  with _ ->
    Kernel.warning "Cannot open configuration file %a\n" Filepath.pretty_abs fname


(** Make some regular expressions early *)
let intRegexp = Str.regexp "i\\([^;]+\\);"
let floatRegexp = Str.regexp "f\\([^;]+\\);"
let boolRegexp = Str.regexp "b\\(\\(true\\)\\|\\(false\\)\\);"
let stringRegexp = Str.regexp "\"\\([^\"]*\\)\""

let loadConfiguration (fname : Filepath.t) : unit =
  H.clear configurationData;

  let stringToConfig (s: string) : configData =
    let idx = ref 0 in (* the current index *)
    let l = String.length s in

    let rec getOne () : configData =
      if !idx >= l then raise Not_found;
      if Str.string_match intRegexp s !idx then begin
        idx := Str.match_end ();
        let p = Str.matched_group 1 s in
        (try ConfInt (int_of_string p)
         with Failure _ ->
           Kernel.warning "Invalid integer configuration element %s" p;
           raise Not_found)
      end else if Str.string_match floatRegexp s !idx then begin
        idx := Str.match_end ();
        let p = Str.matched_group 1 s in
        (try ConfFloat (float_of_string p)
         with Failure _ ->
           Kernel.warning "Invalid float configuration element %s" p;
           raise Not_found)
      end else if Str.string_match boolRegexp s !idx then begin
        idx := Str.match_end ();
        ConfBool (bool_of_string (Str.matched_group 1 s))
      end else if  Str.string_match stringRegexp s !idx then begin
        idx := Str.match_end ();
        ConfString (Str.matched_group 1 s)
      end else if String.get s !idx = '[' then begin
        (* We are starting a list *)
        incr idx;
        let rec loop (acc: configData list) : configData list =
          if !idx >= l then begin
            Kernel.warning "Non-terminated list in configuration %s" s;
            raise Not_found
          end;
          if String.get s !idx = ']' then begin
            incr idx;
            List.rev acc
          end else
            loop (getOne () :: acc)
        in
        ConfList (loop [])
      end else begin
        Kernel.warning "Bad configuration element in a list: %s"
          (String.sub s !idx (l - !idx));
        raise Not_found
      end
    in
    getOne ()
  in
  let open Filesystem.Operators in
  try
    let$ ic = Filesystem.with_open_in_exn fname in
    Kernel.debug "Loading configuration from %a@." Filepath.pretty_abs fname;
    while true do
      let k = input_line ic in
      let s = input_line ic in
      try
        let c = stringToConfig s in
        setConfiguration k c
      with Not_found -> ()
    done
  with End_of_file | Sys_error _ -> ()