misc.mli 4.67 KB
Newer Older
1
2
(**************************************************************************)
(*                                                                        *)
Patrick Baudin's avatar
Patrick Baudin committed
3
(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
4
(*                                                                        *)
5
(*  Copyright (C) 2012-2019                                               *)
Virgile Prevosto's avatar
Virgile Prevosto committed
6
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
Julien Signoles's avatar
Julien Signoles committed
7
(*         alternatives)                                                  *)
8
9
10
11
12
13
14
15
16
17
18
(*                                                                        *)
(*  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                 *)
Virgile Prevosto's avatar
Virgile Prevosto committed
19
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
20
21
22
23
24
25
26
27
28
29
30
(*                                                                        *)
(**************************************************************************)

(** Utilities for E-ACSL. *)

open Cil_types

(* ************************************************************************** *)
(** {2 Builders} *)
(* ************************************************************************** *)

Julien Signoles's avatar
Julien Signoles committed
31
exception Unregistered_library_function of string
32
33
34
val get_lib_fun_vi: string -> varinfo
(** Return varinfo corresponding to a name of a given library function *)

35
36
37
(* ************************************************************************** *)
(** {2 Handling \result} *)
(* ************************************************************************** *)
38
39
40
41
42
43

val result_lhost: kernel_function -> lhost
(** @return the lhost corresponding to \result in the given function *)

val result_vi: kernel_function -> varinfo
(** @return the varinfo corresponding to \result in the given function *)
44

45
46
47
48
49
50
51
52
53
(* ************************************************************************** *)
(** {2 Handling the E-ACSL's C-libraries} *)
(* ************************************************************************** *)

val library_files: unit -> string list
val is_library_loc: location -> bool
val register_library_function: varinfo -> unit
val reset: unit -> unit

54
55
val is_fc_or_compiler_builtin: varinfo -> bool

56
57
58
59
60
(* ************************************************************************** *)
(** {2 Other stuff} *)
(* ************************************************************************** *)

val term_addr_of: loc:location -> term_lval -> typ -> term
61

62
63
64
65
66
val reorder_ast: unit -> unit
(* Reorder current AST by bringing all global declarations belonging to the
 * E-ACSL runtime library and their dependencies (e.g., typedef size_t) to
 * the very top of the file. *)

Julien Signoles's avatar
Julien Signoles committed
67
val cty: logic_type -> typ
68
(** Assume that the logic type is indeed a C type. Just return it. *)
Julien Signoles's avatar
Julien Signoles committed
69

70
val ptr_index: ?loc:location -> ?index:exp -> exp
71
72
  -> Cil_types.exp * Cil_types.exp
(** Split pointer-arithmetic expression of the type `p + i` into its
73
    pointer and integer parts. *)
74

75
val term_of_li: logic_info -> term
76
(** [term_of_li li] assumes that [li.l_body] matches [LBterm t]
77
    and returns [t]. *)
78

79
val is_set_of_ptr_or_array: logic_type -> bool
80
(** Checks whether the given logic type is a set of pointers. *)
81
82

val is_range_free: term -> bool
83
(** Returns [true] iff the given term does not contain any range. *)
84

85
val is_bitfield_pointers: logic_type -> bool
86
(** Returns [true] iff the given logic type is a bitfield pointer or a
Julien Signoles's avatar
Julien Signoles committed
87
    set of bitfield pointers. *)
88

89
val term_has_lv_from_vi: term -> bool
90
(** Return [true] iff the given term contains a variables that originates from
Julien Signoles's avatar
Julien Signoles committed
91
    a C varinfo, that is a non-purely logic variable. *)
92
93
94

type pred_or_term = PoT_pred of predicate | PoT_term of term

95
val mk_ptr_sizeof: typ -> location -> exp
96
(** [mk_ptr_sizeof ptr_typ loc] takes the pointer typ [ptr_typ] that points
97
98
99
100
    to a [typ] typ and returns [sizeof(typ)]. *)

val name_of_binop: binop -> string
(** Returns the name of the given binop as a string *)
101

102
val finite_min_and_max: Ival.t -> Integer.t * Integer.t
103
104
(** [finite_min_and_max i] takes the finite ival [i] and returns its bounds *)

105
106
(*
Local Variables:
107
compile-command: "make -C ../../../../.."
108
End:
109
*)