functor
(Value : Abstract_value.S) (Loc : sig
type value = Value.t
type location
type offset
val equal_loc :
location -> location -> bool
val equal_offset :
offset -> offset -> bool
val pretty_loc :
Format.formatter -> location -> unit
val pretty_offset :
Format.formatter -> offset -> unit
val to_value : location -> value
val size : location -> Int_Base.t
val partially_overlap :
location -> location -> bool
val check_non_overlapping :
(Cil_types.lval * location) list ->
(Cil_types.lval * location) list ->
unit Eval.evaluated
val offset_cardinal_zero_or_one :
offset -> bool
val no_offset : offset
val forward_field :
Cil_types.typ ->
Cil_types.fieldinfo ->
offset -> offset
val forward_index :
Cil_types.typ ->
value -> offset -> offset
val reduce_index_by_array_size :
size_expr:Cil_types.exp ->
index_expr:Cil_types.exp ->
Integer.t ->
value -> value Eval.evaluated
val forward_variable :
Cil_types.typ ->
Cil_types.varinfo ->
offset -> location Eval.or_bottom
val forward_pointer :
Cil_types.typ ->
value ->
offset -> location Eval.or_bottom
val eval_varinfo :
Cil_types.varinfo -> location
val reduce_loc_by_validity :
for_writing:bool ->
bitfield:bool ->
Cil_types.lval ->
location -> location Eval.evaluated
val backward_variable :
Cil_types.varinfo ->
location -> offset Eval.or_bottom
val backward_pointer :
value ->
offset ->
location ->
(value * offset) Eval.or_bottom
val backward_field :
Cil_types.typ ->
Cil_types.fieldinfo ->
offset -> offset Eval.or_bottom
val backward_index :
Cil_types.typ ->
index:value ->
remaining:offset ->
offset ->
(value * offset) Eval.or_bottom
end) (Domain : sig
type state
type t = state
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr :
Structural_descr.pack
val reprs : t list
val equal :
t -> t -> bool
val compare :
t -> t -> int
val hash : t -> int
val pretty_code :
Format.formatter ->
t -> unit
val internal_pretty_code :
Type.precedence ->
Format.formatter ->
t -> unit
val pretty :
Format.formatter ->
t -> unit
val varname :
t -> string
val mem_project :
(Project_skeleton.t ->
bool) ->
t -> bool
val copy : t -> t
module Set :
sig
type elt = t
type t
val empty : t
val is_empty :
t -> bool
val mem :
elt -> t -> bool
val add :
elt -> t -> t
val singleton :
elt -> t
val remove :
elt -> t -> t
val union :
t -> t -> t
val inter :
t -> t -> t
val diff :
t -> t -> t
val subset :
t -> t -> bool
val iter :
(elt -> unit) ->
t -> unit
val fold :
(elt -> 'a -> 'a) ->
t -> 'a -> 'a
val for_all :
(elt -> bool) ->
t -> bool
val exists :
(elt -> bool) ->
t -> bool
val filter :
(elt -> bool) ->
t -> t
val partition :
(elt -> bool) ->
t -> t * t
val cardinal :
t -> int
val elements :
t -> elt list
val choose :
t -> elt
val split :
elt ->
t -> t * bool * t
val find :
elt -> t -> elt
val of_list :
elt list -> t
val min_elt :
t -> elt
val max_elt :
t -> elt
val nearest_elt_le :
elt -> t -> elt
val nearest_elt_ge :
elt -> t -> elt
val ty : t Type.t
val name : string
val descr :
t Descr.t
val packed_descr :
Structural_descr.pack
val reprs : t list
val equal :
t -> t -> bool
val compare :
t -> t -> int
val hash : t -> int
val pretty_code :
Format.formatter ->
t -> unit
val internal_pretty_code :
Type.precedence ->
Format.formatter ->
t -> unit
val pretty :
Format.formatter ->
t -> unit
val varname :
t -> string
val mem_project :
(Project_skeleton.t ->
bool) ->
t -> bool
val copy : t -> t
end
module Map :
sig
type key = t
type +'a t
val empty : 'a t
val is_empty :
'a t -> bool
val mem :
key ->
'a t -> bool
val add :
key ->
'a -> 'a t -> 'a t
val singleton :
key -> 'a -> 'a t
val remove :
key ->
'a t -> 'a t
val merge :
(key ->
'a option ->
'b option ->
'c option) ->
'a t ->
'b t -> 'c t
val compare :
('a -> 'a -> int) ->
'a t ->
'a t -> int
val equal :
('a -> 'a -> bool) ->
'a t ->
'a t -> bool
val iter :
(key -> 'a -> unit) ->
'a t -> unit
val fold :
(key ->
'a -> 'b -> 'b) ->
'a t -> 'b -> 'b
val for_all :
(key -> 'a -> bool) ->
'a t -> bool
val exists :
(key -> 'a -> bool) ->
'a t -> bool
val filter :
(key -> 'a -> bool) ->
'a t -> 'a t
val partition :
(key -> 'a -> bool) ->
'a t ->
'a t * 'a t
val cardinal :
'a t -> int
val bindings :
'a t ->
(key * 'a) list
val min_binding :
'a t -> key * 'a
val max_binding :
'a t -> key * 'a
val choose :
'a t -> key * 'a
val split :
key ->
'a t ->
'a t * 'a option *
'a t
val find :
key -> 'a t -> 'a
val map :
('a -> 'b) ->
'a t -> 'b t
val mapi :
(key -> 'a -> 'b) ->
'a t -> 'b t
module Key :
sig
type t = key
val ty :
t Type.t
val name :
string
val descr :
t Descr.t
val packed_descr :
Structural_descr.pack
val reprs :
t list
val equal :
t -> t -> bool
val compare :
t -> t -> int
val hash :
t -> int
val pretty_code :
Format.formatter ->
t -> unit
val internal_pretty_code :
Type.precedence ->
Format.formatter ->
t -> unit
val pretty :
Format.formatter ->
t -> unit
val varname :
t -> string
val mem_project :
(Project_skeleton.t ->
bool) ->
t -> bool
val copy :
t -> t
end
module Make :
functor
(Data : Datatype.S) ->
sig
type t =
Data.t t
val ty :
t Type.t
val name :
string
val descr :
t Descr.t
val packed_descr :
Structural_descr.pack
val reprs :
t list
val equal :
t ->
t -> bool
val compare :
t ->
t -> int
val hash :
t -> int
val pretty_code :
Format.formatter ->
t -> unit
val internal_pretty_code :
Type.precedence ->
Format.formatter ->
t -> unit
val pretty :
Format.formatter ->
t -> unit
val varname :
t -> string
val mem_project :
(Project_skeleton.t ->
bool) ->
t -> bool
val copy :
t -> t
end
end
module Hashtbl :
sig
type key = t
type 'a t
val create :
int -> 'a t
val clear :
'a t -> unit
val reset :
'a t -> unit
val copy :
'a t -> 'a t
val add :
'a t ->
key -> 'a -> unit
val remove :
'a t ->
key -> unit
val find :
'a t -> key -> 'a
val find_all :
'a t ->
key -> 'a list
val replace :
'a t ->
key -> 'a -> unit
val mem :
'a t ->
key -> bool
val iter :
(key -> 'a -> unit) ->
'a t -> unit
val filter_map_inplace :
(key ->
'a -> 'a option) ->
'a t -> unit
val fold :
(key ->
'a -> 'b -> 'b) ->
'a t -> 'b -> 'b
val length :
'a t -> int
val stats :
'a t ->
Hashtbl.statistics
val iter_sorted :
?cmp:(key ->
key -> int) ->
(key -> 'a -> unit) ->
'a t -> unit
val fold_sorted :
?cmp:(key ->
key -> int) ->
(key ->
'a -> 'b -> 'b) ->
'a t -> 'b -> 'b
val iter_sorted_by_entry :
cmp:(key * 'a ->
key * 'a ->
int) ->
(key -> 'a -> unit) ->
'a t -> unit
val fold_sorted_by_entry :
cmp:(key * 'a ->
key * 'a ->
int) ->
(key ->
'a -> 'b -> 'b) ->
'a t -> 'b -> 'b
val iter_sorted_by_value :
cmp:('a ->
'a -> int) ->
(key -> 'a -> unit) ->
'a t -> unit
val fold_sorted_by_value :
cmp:('a ->
'a -> int) ->
(key ->
'a -> 'b -> 'b) ->
'a t -> 'b -> 'b
val structural_descr :
Structural_descr.t ->
Structural_descr.t
val make_type :
'a Type.t ->
'a t Type.t
val memo :
'a t ->
key ->
(key -> 'a) -> 'a
module Key :
sig
type t = key
val ty :
t Type.t
val name :
string
val descr :
t Descr.t
val packed_descr :
Structural_descr.pack
val reprs :
t list
val equal :
t -> t -> bool
val compare :
t -> t -> int
val hash :
t -> int
val pretty_code :
Format.formatter ->
t -> unit
val internal_pretty_code :
Type.precedence ->
Format.formatter ->
t -> unit
val pretty :
Format.formatter ->
t -> unit
val varname :
t -> string
val mem_project :
(Project_skeleton.t ->
bool) ->
t -> bool
val copy :
t -> t
end
module Make :
functor
(Data : Datatype.S) ->
sig
type t =
Data.t t
val ty :
t Type.t
val name :
string
val descr :
t Descr.t
val packed_descr :
Structural_descr.pack
val reprs :
t list
val equal :
t ->
t -> bool
val compare :
t ->
t -> int
val hash :
t -> int
val pretty_code :
Format.formatter ->
t -> unit
val internal_pretty_code :
Type.precedence ->
Format.formatter ->
t -> unit
val pretty :
Format.formatter ->
t -> unit
val varname :
t -> string
val mem_project :
(Project_skeleton.t ->
bool) ->
t -> bool
val copy :
t -> t
end
end
val top : t
val is_included :
t -> t -> bool
val join : t -> t -> t
val join_and_is_included :
t -> t -> t * bool
val widen :
Cil_types.kernel_function ->
Cil_types.stmt ->
t -> t -> t
type value = Value.t
type location =
Loc.location
type origin
val extract_expr :
(Cil_types.exp ->
value Eval.evaluated) ->
t ->
Cil_types.exp ->
(value * origin)
Eval.evaluated
val extract_lval :
(Cil_types.exp ->
value Eval.evaluated) ->
t ->
Cil_types.lval ->
Cil_types.typ ->
location ->
(value * origin)
Eval.evaluated
val backward_location :
t ->
Cil_types.lval ->
Cil_types.typ ->
location ->
value ->
(location * value)
Eval.or_bottom
val reduce_further :
t ->
Cil_types.exp ->
value ->
(Cil_types.exp * value)
list
module Transfer :
functor
(Valuation :
sig
type t
type value = value
type origin =
origin
type loc =
location
val find :
t ->
Cil_types.exp ->
(value, origin)
Eval.record_val
Eval.or_top
val fold :
(Cil_types.exp ->
(value, origin)
Eval.record_val ->
'a -> 'a) ->
t -> 'a -> 'a
val find_loc :
t ->
Cil_types.lval ->
loc
Eval.record_loc
Eval.or_top
end) ->
sig
type state = t
type value = value
type location =
location
type valuation =
Valuation.t
val update :
valuation ->
state -> state
val assign :
Cil_types.kinstr ->
location
Eval.left_value ->
Cil_types.exp ->
value
Eval.assigned ->
valuation ->
state ->
state
Eval.or_bottom
val assume :
Cil_types.stmt ->
Cil_types.exp ->
bool ->
valuation ->
state ->
state
Eval.or_bottom
val start_call :
Cil_types.stmt ->
value Eval.call ->
valuation ->
state ->
state
Eval.call_action
val finalize_call :
Cil_types.stmt ->
value Eval.call ->
pre:state ->
post:state ->
state
Eval.or_bottom
val approximate_call :
Cil_types.stmt ->
value Eval.call ->
state ->
state list
Eval.or_bottom
end
val compute_using_specification :
Cil_types.kinstr ->
value Eval.call ->
Cil_types.funspec ->
state ->
state list
Eval.or_bottom
type eval_env
val env_current_state :
eval_env ->
t Eval.or_bottom
val env_annot :
pre:t ->
here:t ->
unit -> eval_env
val env_pre_f :
pre:t ->
unit -> eval_env
val env_post_f :
pre:t ->
post:t ->
result:Cil_types.varinfo
option ->
unit -> eval_env
val eval_predicate :
eval_env ->
Cil_types.predicate ->
Alarmset.status
val reduce_by_predicate :
eval_env ->
bool ->
Cil_types.predicate ->
eval_env
val enter_scope :
Cil_types.kernel_function ->
Cil_types.varinfo list ->
t -> t
val leave_scope :
Cil_types.kernel_function ->
Cil_types.varinfo list ->
t -> t
val enter_loop :
Cil_types.stmt ->
state -> state
val incr_loop_counter :
Cil_types.stmt ->
state -> state
val leave_loop :
Cil_types.stmt ->
state -> state
val empty : unit -> t
val initialize_var :
t ->
Cil_types.lval ->
location ->
(value * bool)
Eval.or_bottom ->
t
val initialize_var_using_type :
t ->
Cil_types.varinfo -> t
val global_state :
unit ->
t Eval.or_bottom
option
val filter_by_bases :
Base.Hptset.t ->
t -> t
val reuse :
current_input:
t ->
previous_output:t -> t
val structure :
t
Abstract_domain.structure
module Store :
sig
val register_initial_state :
Value_types.callstack ->
state -> unit
val register_state_before_stmt :
Value_types.callstack ->
Cil_types.stmt ->
state -> unit
val register_state_after_stmt :
Value_types.callstack ->
Cil_types.stmt ->
state -> unit
val get_initial_state :
Cil_types.kernel_function ->
state
Eval.or_bottom
val get_initial_state_by_callstack :
Cil_types.kernel_function ->
state
Value_types.Callstack.Hashtbl.t
option
val get_stmt_state :
Cil_types.stmt ->
state
Eval.or_bottom
val get_stmt_state_by_callstack :
after:bool ->
Cil_types.stmt ->
state
Value_types.Callstack.Hashtbl.t
option
end
val mem :
'a Abstract_domain.key ->
bool
val get :
'a Abstract_domain.key ->
(state -> 'a) option
val set :
'a Abstract_domain.key ->
'a -> state -> state
end) (Eva : sig
type state =
Domain.state
type value =
Domain.value
type origin =
Domain.origin
type loc =
Domain.location
module Valuation :
sig
type t
type value =
value
type origin =
origin
type loc =
loc
val empty :
t
val find :
t ->
Cil_types.exp ->
(value,
origin)
Eval.record_val
Eval.or_top
val add :
t ->
Cil_types.exp ->
(value,
origin)
Eval.record_val ->
t
val fold :
(Cil_types.exp ->
(value,
origin)
Eval.record_val ->
'a -> 'a) ->
t ->
'a -> 'a
val find_loc :
t ->
Cil_types.lval ->
loc
Eval.record_loc
Eval.or_top
val remove :
t ->
Cil_types.exp ->
t
val remove_loc :
t ->
Cil_types.lval ->
t
end
val evaluate :
?valuation:
Valuation.t ->
?reduction:
bool ->
state ->
Cil_types.exp ->
(Valuation.t *
value)
Eval.evaluated
val copy_lvalue :
?valuation:
Valuation.t ->
state ->
Cil_types.lval ->
(Valuation.t *
value
Eval.flagged_value)
Eval.evaluated
val lvaluate :
?valuation:
Valuation.t ->
for_writing:
bool ->
state ->
Cil_types.lval ->
(Valuation.t *
loc *
Cil_types.typ)
Eval.evaluated
val can_copy :
?valuation:
Valuation.t ->
is_ret:
bool ->
state ->
Kernel_function.t ->
Cil_types.lval ->
Cil_types.exp ->
(Cil_types.lval
option *
Valuation.t)
Eval.evaluated
val reduce :
?valuation:
Valuation.t ->
state ->
Cil_types.exp ->
bool ->
Valuation.t
Eval.evaluated
val assume :
?valuation:
Valuation.t ->
state ->
Cil_types.exp ->
value ->
Valuation.t
Eval.or_bottom
val split_by_evaluation :
Cil_types.exp ->
Integer.t
list ->
state list ->
(Integer.t *
state
list *
bool)
list *
state list
val check_copy_lval :
Cil_types.lval *
loc ->
Cil_types.lval *
loc ->
bool
Eval.evaluated
val check_non_overlapping :
state ->
Cil_types.lval
list ->
Cil_types.lval
list ->
unit
Eval.evaluated
val eval_function_exp :
Cil_types.exp ->
state ->
(Kernel_function.t *
Valuation.t)
list
Eval.evaluated
end) ->
sig
val initial_state : lib_entry:bool -> Domain.t Bottom.Type.or_bottom
val initial_state_with_formals :
lib_entry:bool ->
Cil_types.kernel_function -> Domain.t Bottom.Type.or_bottom
val initialize_var :
with_alarms:CilE.warn_mode ->
Cil_types.stmt ->
Cil_types.varinfo ->
Cil_types.init -> Domain.t -> Domain.t Bottom.Type.or_bottom
end