emitter.mli 6.76 KB
Newer Older
1
2
3
4
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
Andre Maroneze's avatar
Andre Maroneze committed
5
(*  Copyright (C) 2007-2020                                               *)
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
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

(** Emitter. An emitter is the Frama-C entity which is able to emit annotations
    and property status. Thus you have to create (at least) one of your own if
    you want to do such tasks.
    @since Nitrogen-20111001 *)

(**************************************************************************)
(** {2 API for Plug-ins Developers} *)
(**************************************************************************)

type emitter
type kind = Property_status | Alarm | Code_annot | Funspec | Global_annot
(** When selecting [Alarm], [Code_annot] is also automatically selected *)

include Datatype.S_with_collections with type t = emitter

val create: 
  string -> 
  kind list -> 
  correctness:Typed_parameter.t list -> 
  tuning:Typed_parameter.t list -> t
(** [Emitter.create name kind ~correctness ~tuning] creates a new emitter with
    the given name. The given parameters are the ones which impact the generated
    annotations/status. A "correctness" parameter may fully change a generated
    element when its value changes (for instance, a valid status may become
    invalid and conversely). A "tuning" parameter may improve a generated
    element when its value changes (for instance, a "dont_know" status may
    become valid or invalid, but a valid status cannot become invalid).
    The given name must be unique.
    @raise Invalid_argument if an emitter with the given name already exist 
    @plugin development guide *)

val get_name: t -> string

val correctness_parameters: t -> string list
val tuning_parameters: t -> string list

val end_user: t
(** The special emitter corresponding to the end-user. Only the kernel should
    use this emitter when emitting annotations or statuses.
    @since Oxygen-20120901 *)

val kernel: t
(** The special emitter corresponding to the kernel. Only the kernel should
    use this emitter when emitting annotations or statuses.
    @since Oxygen-20120901 *)

69
70
71
72
73
val orphan: t
  (** special emitter for adopting annotations that were generated by an
      emitter that is no longer available (in particular, annotations loaded
      from a state that was generated from a different set of plug-ins than
      in current session). Should not be used outside of the kernel.
74
      @since 22.0-Titanium
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
(** Usable emitters are the ones which can really emit something. *)
module Usable_emitter: sig
  include Datatype.S_with_collections
  val get: t -> emitter
  (** Get the emitter from an usable emitter. Not so efficient. 
      @since Oxygen-20120901 *)

  val get_name: t -> string
  val get_unique_name: t -> string
  val correctness_parameters: t -> string list
  val tuning_parameters: t -> string list
  val pretty_parameter: Format.formatter -> tuning:bool -> t -> string -> unit
(** Pretty print the parameter (given by its name) with its value.
    @raise Not_found if the parameter is not one of the given emitter *)
end

val distinct_tuning_parameters: Usable_emitter.t -> Datatype.String.Set.t
(** Return the tuning parameter which distinguishes this usable emitter from the
    other ones.
    @since Oxygen-20120901 *)

val distinct_correctness_parameters: Usable_emitter.t -> Datatype.String.Set.t
(** Return the correctness_parameters which distinguishes this usable emitter
    from the other ones.
    @since Oxygen-20120901 *)

(* ********************************************************************** *)
(** {2 Kernel Internal API} *)
(* ********************************************************************** *)

val get: t -> Usable_emitter.t
(** Get the emitter which is really able to emit something. 
    This function must be called at the time of the emission. No action must
    occur between the call to [get] and the emission (in particular no update
    of any parameter of the emitter. *)

val self: State.t

val dummy: t

(** Table indexing: key -> emitter (or equivalent data) -> value.
    Quick access + handle cleaning in the right way (only remove relevant
    bindings when required. 
    @since Oxygen-20120901 *)
module Make_table
  (H: Datatype.Hashtbl)
  (E: sig 
    include Datatype.S_with_collections
    val local_clear: H.key -> 'a Hashtbl.t -> unit
    val usable_get: t -> Usable_emitter.t 
    val get: t -> emitter
  end)
  (D: Datatype.S) 
  (Info: sig include State_builder.Info_with_size val kinds: kind list end) : 
sig
  type internal_tbl = D.t E.Hashtbl.t
  val self: State.t
  val add: H.key -> internal_tbl -> unit
  val find: H.key -> internal_tbl
  val mem: H.key -> bool
  val iter: (H.key -> internal_tbl -> unit) -> unit
  val fold: (H.key -> internal_tbl -> 'a -> 'a) -> 'a -> 'a
  val iter_sorted:
    cmp: (H.key -> H.key -> int) -> (H.key -> internal_tbl -> unit) -> unit
  val fold_sorted:
    cmp: (H.key -> H.key -> int) ->
    (H.key -> internal_tbl -> 'a -> 'a) -> 'a -> 'a
  val remove: H.key -> unit
  val add_hook_on_remove: (E.t -> H.key -> D.t -> unit) -> unit
(** Register a hook to be applied whenever a binding is removed from the table.
    @since Fluorine-20130401 *)
  val apply_hooks_on_remove: E.t -> H.key -> D.t -> unit
(** This function must be called on each binding which is removed from the
    table without directly calling the function {!remove}.
    @since Fluorine-20130401 *)
end

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