1
(**************************************************************************)
3
(* This file is part of Frama-C. *)
5
(* Copyright (C) 2007-2008 *)
6
(* CEA (Commissariat � l'�nergie Atomique) *)
8
(* you can redistribute it and/or modify it under the terms of the GNU *)
9
(* Lesser General Public License as published by the Free Software *)
10
(* Foundation, version 2.1. *)
12
(* It is distributed in the hope that it will be useful, *)
13
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
14
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
15
(* GNU Lesser General Public License for more details. *)
17
(* See the GNU Lesser General Public License version 2.1 *)
18
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
20
(**************************************************************************)
22
(*i $Id: lmap.mli,v 1.71 2008/11/18 12:13:41 uid568 Exp $ i*)
24
(** Functors making map indexed by locations.
25
@plugin development guide *)
34
module type Location_map =
36
type y (** type of the values associated to the locations *)
38
type widen_hint_offsetmap
39
(* module LOffset : Offsetmap.S with type y = y
40
and type widen_hint = widen_hint_offsetmap
43
(Default_offsetmap: sig val default_offsetmap : Base.t -> loffset end):
45
type t (** the type of a map *)
47
type widen_hint = bool * BaseSet.t * (Base.t -> widen_hint_offsetmap)
49
type instanciation = Location_Bytes.t BaseMap.t
51
module Datatype : Project.Datatype.S with type t = t
53
val inject : Base.t -> loffset -> t
55
val add_offsetmap : Base.t -> loffset -> t -> t
57
val pretty : Format.formatter -> t -> unit
58
val pretty_without_null : Format.formatter -> t -> unit
59
val pretty_filter: Format.formatter -> t -> Locations.Zone.t -> unit
61
with_alarms:CilE.warn_mode -> exact:bool -> t -> location -> y -> t
63
val find : with_alarms:CilE.warn_mode -> t -> location -> y
65
val join : t -> t -> t
66
val is_included : t -> t -> bool
67
val equal : t -> t -> bool
69
val is_included_actual_generic :
70
Zone.t -> t -> t -> instanciation
72
(** Every location is associated to [VALUE.top] in [empty].*)
74
val is_empty : t -> bool
76
(** Every location is associated to [VALUE.bottom] in [bottom].
77
This state can be reached only in dead code. *)
79
val is_reachable : t -> bool
81
val widen : widen_hint-> t -> t -> (bool * t)
84
val filter_base : (Base.t -> bool) -> t -> t
86
(** @raise Not_found if the varid is not present in the map. *)
87
val find_base : Base.t -> t -> loffset
89
(** Removes the base if it is present. Does nothing otherwise. *)
90
val remove_base : Base.t -> t -> t
93
(** [copy_paste src dst state] returns a modified version of [state] in
94
which everything present in [src] has been copied onto [dst]. [src] and
95
[dst] must have the same size. The write operation is exact iff [dst]
97
@raise Cannot_copy if copy is not possible. *)
98
val copy_paste : location -> location -> t -> t
100
(** @raise Cannot_copy if copy is not possible. *)
101
val paste_offsetmap :
102
loffset -> Location_Bits.t -> Int.t -> Int.t -> t -> t
104
(** May return [None] as a bottom loffset.
105
@raise Cannot_copy if copy is not possible. *)
106
val copy_offsetmap : Locations.location -> t -> loffset option
108
val compute_actual_final_from_generic :
109
t -> t -> Locations.Zone.t -> instanciation -> t*Location_Bits.Top_Param.t
111
val is_included_by_location_enum : t -> t -> Locations.Zone.t -> bool
113
(** @raise Invalid_argument if one location is not aligned or of size
115
@raise Error_Bottom if [m] is bottom. *)
116
val fold : size:Int.t -> (location -> y -> 'a -> 'a) -> t -> 'a -> 'a
119
(** [fold_base f m] calls [f] on all bases bound to non top
120
offsetmaps in the non bottom map [m].
121
@raise Error_Bottom if [m] is bottom. *)
122
val fold_base : (Base.t -> 'a -> 'a) -> t -> 'a -> 'a
124
(** [fold_base_offsetmap f m] calls [f] on all bases bound to non
125
top offsetmaps in the non bottom map [m].
126
@raise Error_Bottom if [m] is bottom.*)
127
val fold_base_offsetmap : (Base.t -> loffset -> 'a -> 'a) -> t -> 'a -> 'a
129
val find_offsetmap_for_location : Location_Bits.t -> t -> loffset
130
val add_whole: location -> y -> t -> t
131
val remove_whole: location -> t -> t
133
(** [reciprocal_image m b] is the set of bits in the map [m] that may lead
134
to Top([b]) and the location in [m] where one may read an address
136
val reciprocal_image : Base.t -> t -> Zone.t*Location_Bits.t
138
val create_initialized_var :
139
Cil_types.varinfo -> Base.validity -> loffset -> Base.t
146
exception Error_Bottom
149
f:(Base.t -> loffset -> 'a) ->
150
cache:string * int -> joiner:('a -> 'a -> 'a) -> empty:'a -> t -> 'a
153
f:(Base.t -> loffset -> loffset) ->
154
cache:string * int ->
160
(VALUE:Lattice_With_Isotropy.S)
161
(LOffset:Offsetmap.S with type y = VALUE.t
162
and type widen_hint = VALUE.widen_hint) :
163
Location_map with type y = VALUE.t
164
and type widen_hint_offsetmap = VALUE.widen_hint
165
and type loffset = LOffset.t
added
removed
src/memory_state/lmap.mli
