lannot/annotators.mli at main · kidq330/lannot · GitHub

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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of the Frama-C's Lannotate plug-in.                 *)
(*                                                                        *)
(*  Copyright (C) 2012-2022                                               *)
(*    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 LICENSE)                       *)
(*                                                                        *)
(**************************************************************************)

type annotation =
  int * string * Cil_types.exp * Cil_types.location

type annotator

(** Module type of annotators *)
module type ANNOTATOR = sig
  val name : string
  val help : string

  (** Insert IN PLACE the annotation on the given AST.

      In addition of the AST, it also takes a function as parameter.
      This function is provided by Annotators, it makes a label statement
      from a boolean condition and an "origin" location (e.g. the
      if-then-else condition's location in the case of a MCC label).
  *)
  val apply : (Cil_types.exp -> Cil_types.exp list -> Cil_types.location -> Cil_types.stmt) -> Cil_types.file -> unit
end

module type ANNOTATOR_WITH_EXTRA_TAGS = sig
  val name : string
  val help : string
  val apply : (extra:string list -> Cil_types.exp -> Cil_types.exp list -> Cil_types.location -> Cil_types.stmt) -> Cil_types.file -> unit
end

module type S = sig
  val self : annotator
  val apply : ?id:(unit -> int) -> ?collect:(annotation -> unit) -> Cil_types.file -> unit
end

(**
   Register an annotator
*)
module Register (_ : ANNOTATOR) : S

(**
   Register an annotator that provides extra tags (for instance, mutator tags)
   in addition of the annotator name
*)
module RegisterWithExtraTags (_ : ANNOTATOR_WITH_EXTRA_TAGS) : S

val get_file_name : unit -> string

val annotate_with : annotator -> ?id:(unit -> int) -> ?collect:(annotation -> unit) -> Cil_types.file -> unit

val annotate : string -> string list -> ?id:(unit->int) -> ?collect:(annotation -> unit) -> Cil_types.file -> unit

val shouldInstrumentFun : Cil_types.varinfo -> bool
val shouldInstrumentVar : Cil_types.varinfo -> bool

val print_help : Format.formatter -> unit

val getCurrentLabelId : unit -> int
val getCurrentBindingId: unit -> int
val getCurrentHLId: unit -> int

val pc_label : Cil_types.varinfo option ref
val pc_label_bindings : Cil_types.varinfo option ref
val mutated : Cil_types.varinfo option ref
val label_function_vinfo : Cil_types.varinfo option ref
val init_builtins : unit -> unit

val next : unit -> int
val next_hl: unit -> string
val next_binding: unit -> int