File: kernel.ml

package info (click to toggle)
frama-c 20100401%2Bboron%2Bdfsg-5
  • links: PTS, VCS
  • area: main
  • in suites: squeeze
  • size: 12,908 kB
  • ctags: 19,772
  • sloc: ml: 117,445; ansic: 10,764; makefile: 1,706; lisp: 176; sh: 27
file content (89 lines) | stat: -rw-r--r-- 3,585 bytes parent folder | download
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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2010                                               *)
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

module type Parameter_input = sig
  include Plugin.Parameter_input
  val module_name: string
end

module type Parameter_input_with_arg = sig
  include Plugin.Parameter_input_with_arg
  val module_name: string
end

module type COMPLEX_VALUE = sig
  include Plugin.COMPLEX_VALUE
  val module_name: string
end

let () = Plugin.register_kernel ()

module P = Plugin.Register
  (struct
     let name = ""
     let shortname = ""
     let module_name = ""
     let descr = "General options provided by the Frama-C kernel"
   end)

include (P: Plugin.S)

module Bool(X:sig include Parameter_input val default: bool end) =
  P.Bool(struct let () = Plugin.set_module_name X.module_name include X end)

module False(X: Parameter_input) =
  P.False(struct let () = Plugin.set_module_name X.module_name include X end)

module True(X: Parameter_input) =
  P.True(struct let () = Plugin.set_module_name X.module_name include X end)

module Int (X: sig val default: int include Parameter_input_with_arg end) =
  P.Int(struct let () = Plugin.set_module_name X.module_name include X end)

module Zero(X:Parameter_input_with_arg) =
  P.Zero(struct let () = Plugin.set_module_name X.module_name include X end)

module String
  (X: sig include Parameter_input_with_arg val default: string end) =
  P.String(struct let () = Plugin.set_module_name X.module_name include X end)

module EmptyString(X: Parameter_input_with_arg) =
  P.EmptyString
    (struct let () = Plugin.set_module_name X.module_name include X end)

module StringSet(X: Parameter_input_with_arg) =
  P.StringSet
    (struct let () = Plugin.set_module_name X.module_name include X end)

module StringList(X: Parameter_input_with_arg) =
  P.StringList
    (struct let () = Plugin.set_module_name X.module_name include X end)

module IndexedVal (V:COMPLEX_VALUE) =
  P.IndexedVal
    (struct let () = Plugin.set_module_name V.module_name include V end)

(*
Local Variables:
compile-command: "LC_ALL=C make -C ../.."
End:
*)