lannot/utils.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
(**************************************************************************)
(*                                                                        *)
(*  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)                       *)
(*                                                                        *)
(**************************************************************************)

open Cil_types

module Printer : Printer_api.S

val extract_global_vars : file -> varinfo list
val print_file_path : Cil_types.location -> string
val mk_call :
  ?loc:location -> ?result:lval -> varinfo option -> exp list -> stmt

(** Indicates whether an instruction is a label. *)
val is_label : instr -> bool

(**
   Indicates whether an expression is boolean in itself.
   Used to detect boolean expression outside conditional statement
*)
val is_boolean: exp -> bool

(**
   Get atomic conditons form a boolean expression.
*)
val atomic_conditions : exp -> exp list

(** [combine n l] computes the combinations of [n] elements from the list [l].

    Returns the combination in the order of the list [l] and in a depth-first
    manner. For instance, [combine 2 [1;2;3]] returns [[1;2];[1;3];[2;3]].
*)
val combine : int -> 'a list -> 'a list list

(**
   [rev_combine n l] computes the combinations of [n] elements
   from the list [l].

   Returns the combination in the opposite order of {!combine}.
*)
val rev_combine : int -> 'a list -> 'a list list

(**
   [sign_combine pos neg l] computes all sign combinations of a list of
   elements [l], given two sign functions [pos] and [neg].

   Preserves the original order of the list, i.e. each sublist is
   in the same order.

   For instance, [sign_combine (fun x ->"+"^x) (fun x -> "-"^x) ["1";"2"]]
   returns [["+1";"+2"];["+1";"-2"];["-1";"+2"];["-1";"-2"]].
*)

val sign_combine : pos:('a -> 'b) -> neg:('a -> 'b) -> 'a list -> 'b list list

(**
   [sign_combine pos neg l] computes all sign combinations of a list of
   elements [l], given two sign functions [pos] and [neg].

   Returns the combination in the opposite order of {!sign_combine}.
*)
val rev_sign_combine : pos:('a -> 'b) -> neg:('a -> 'b) -> 'a list -> 'b list list

val get_bounds : ikind -> (binop*exp) list

val is_bound : ikind -> Z.t -> bool