sig
type 'a or_bottom = [ `Bottom | `Value of 'a ]
type 'a or_top = [ `Top | `Value of 'a ]
type 'a or_top_bottom = [ `Bottom | `Top | `Value of 'a ]
module Bottom :
sig
type 'a t = 'a or_bottom
module Operators :
sig
val ( >>- ) : [< 'a t ] -> ('a -> ([> 'b t ] as 'c)) -> 'c
val ( >>-: ) : [< 'a t ] -> ('a -> 'b) -> [> 'b t ]
val ( let+ ) : [< 'a t ] -> ('a -> 'b) -> [> 'b t ]
val ( and+ ) : [< 'a t ] -> [< 'b t ] -> [> ('a * 'b) t ]
val ( let* ) : [< 'a t ] -> ('a -> ([> 'b t ] as 'c)) -> 'c
val ( and* ) : [< 'a t ] -> [< 'b t ] -> [> ('a * 'b) t ]
end
module Make_Datatype :
functor (Domain : Datatype.S) ->
sig
type t = Domain.t or_bottom
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 Bound_Lattice :
functor (Lattice : Lattice_type.Join_Semi_Lattice) ->
sig
type t = Lattice.t or_bottom
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
val join : t -> t -> t
val is_included : t -> t -> bool
val bottom : t
end
val is_bottom : 'a t -> bool
val non_bottom : 'a t -> 'a
val value : bottom:'a -> 'a t -> 'a
val hash : ('a -> int) -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val pretty_bottom : Format.formatter -> unit
val pretty :
(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
val is_included : ('a -> 'b -> bool) -> 'a t -> 'b t -> bool
val join : ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
val join_list : ('a -> 'a -> 'a) -> 'a t list -> 'a t
val narrow : ('a -> 'a -> 'a t) -> 'a t -> 'a t -> 'a t
val iter : ('a -> unit) -> 'a t -> unit
val fold : bottom:'b -> ('a -> 'b) -> 'a t -> 'b
val map : ('a -> 'b) -> 'a t -> 'b t
val zip : 'a t -> 'b t -> ('a * 'b) t
val to_option : 'a t -> 'a option
val of_option : 'a option -> 'a t
val to_list : 'a t -> 'a list
val bot_of_list : 'a list -> 'a list t
val list_of_bot : 'a list t -> 'a list
val list_values : 'a t list -> 'a list
val add_to_list : 'a t -> 'a list -> 'a list
end
module Top :
sig
type 'a t = 'a or_top
module Operators :
sig
val ( >>- ) : [< 'a t ] -> ('a -> ([> 'b t ] as 'c)) -> 'c
val ( >>-: ) : [< 'a t ] -> ('a -> 'b) -> [> 'b t ]
val ( let+ ) : [< 'a t ] -> ('a -> 'b) -> [> 'b t ]
val ( and+ ) : [< 'a t ] -> [< 'b t ] -> [> ('a * 'b) t ]
val ( let* ) : [< 'a t ] -> ('a -> ([> 'b t ] as 'c)) -> 'c
val ( and* ) : [< 'a t ] -> [< 'b t ] -> [> ('a * 'b) t ]
end
val is_top : 'a t -> bool
val non_top : 'a t -> 'a
val value : top:'a -> 'a t -> 'a
val hash : ('a -> int) -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val pretty_top : Format.formatter -> unit
val pretty :
(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
val join : ('a -> 'a -> 'a t) -> 'a t -> 'a t -> 'a t
val narrow : ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
val zip : 'a t -> 'b t -> ('a * 'b) t
val to_option : 'a t -> 'a option
val of_option : 'a option -> 'a t
end
module TopBottom :
sig
type 'a t = 'a or_top_bottom
module Operators :
sig
val ( >>- ) : [< 'a t ] -> ('a -> ([> 'b t ] as 'c)) -> 'c
val ( >>-: ) : [< 'a t ] -> ('a -> 'b) -> [> 'b t ]
val ( let+ ) : [< 'a t ] -> ('a -> 'b) -> [> 'b t ]
val ( and+ ) : [< 'a t ] -> [< 'b t ] -> [> ('a * 'b) t ]
val ( let* ) : [< 'a t ] -> ('a -> ([> 'b t ] as 'c)) -> 'c
val ( and* ) : [< 'a t ] -> [< 'b t ] -> [> ('a * 'b) t ]
end
val hash : ('a -> int) -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val pretty :
(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
val join : ('a -> 'a -> [< 'a t ]) -> 'a t -> 'a t -> 'a t
val narrow : ('a -> 'a -> [< 'a t ]) -> 'a t -> 'a t -> 'a t
end
val ( >>- ) : [< 'a Bottom.t ] -> ('a -> ([> 'b Bottom.t ] as 'c)) -> 'c
val ( >>-: ) : [< 'a Bottom.t ] -> ('a -> 'b) -> [> 'b Bottom.t ]
val ( let+ ) : [< 'a Bottom.t ] -> ('a -> 'b) -> [> 'b Bottom.t ]
val ( and+ ) :
[< 'a Bottom.t ] -> [< 'b Bottom.t ] -> [> ('a * 'b) Bottom.t ]
val ( let* ) : [< 'a Bottom.t ] -> ('a -> ([> 'b Bottom.t ] as 'c)) -> 'c
val ( and* ) :
[< 'a Bottom.t ] -> [< 'b Bottom.t ] -> [> ('a * 'b) Bottom.t ]
type 't with_alarms = 't * Alarmset.t
type 't evaluated = 't or_bottom Eval.with_alarms
val ( >>= ) :
'a Eval.evaluated -> ('a -> 'b Eval.evaluated) -> 'b Eval.evaluated
val ( >>=. ) :
'a Eval.evaluated -> ('a -> 'b or_bottom) -> 'b Eval.evaluated
val ( >>=: ) : 'a Eval.evaluated -> ('a -> 'b) -> 'b Eval.evaluated
type 'a reduced = [ `Bottom | `Unreduced | `Value of 'a ]
type reductness = Unreduced | Reduced | Created | Dull
type 'a flagged_value = {
v : 'a or_bottom;
initialized : bool;
escaping : bool;
}
module Flagged_Value :
sig
val bottom : 'a Eval.flagged_value
val equal :
('a -> 'a -> bool) ->
'a Eval.flagged_value -> 'a Eval.flagged_value -> bool
val join :
('a -> 'a -> 'a) ->
'a Eval.flagged_value ->
'a Eval.flagged_value -> 'a Eval.flagged_value
val pretty :
(Stdlib.Format.formatter -> 'a -> unit) ->
Stdlib.Format.formatter -> 'a Eval.flagged_value -> unit
end
type ('a, 'origin) record_val = {
value : 'a Eval.flagged_value;
origin : 'origin option;
reductness : Eval.reductness;
val_alarms : Alarmset.t;
}
type 'a record_loc = {
loc : 'a;
typ : Cil_types.typ;
loc_alarms : Alarmset.t;
}
module type Valuation =
sig
type t
type value
type origin
type loc
val empty : Eval.Valuation.t
val find :
Eval.Valuation.t ->
Cil_types.exp ->
(Eval.Valuation.value, Eval.Valuation.origin) Eval.record_val or_top
val add :
Eval.Valuation.t ->
Cil_types.exp ->
(Eval.Valuation.value, Eval.Valuation.origin) Eval.record_val ->
Eval.Valuation.t
val fold :
(Cil_types.exp ->
(Eval.Valuation.value, Eval.Valuation.origin) Eval.record_val ->
'a -> 'a) ->
Eval.Valuation.t -> 'a -> 'a
val find_loc :
Eval.Valuation.t ->
Cil_types.lval -> Eval.Valuation.loc Eval.record_loc or_top
val remove : Eval.Valuation.t -> Cil_types.exp -> Eval.Valuation.t
val remove_loc : Eval.Valuation.t -> Cil_types.lval -> Eval.Valuation.t
end
module Clear_Valuation :
functor (Valuation : Valuation) ->
sig
val clear_englobing_exprs :
Eval.Valuation.t ->
expr:Cil_types.exp -> subexpr:Cil_types.exp -> Eval.Valuation.t
end
type 'loc left_value = {
lval : Cil_types.lval;
lloc : 'loc;
ltyp : Cil_types.typ;
}
type ('loc, 'value) assigned =
Assign of 'value
| Copy of 'loc Eval.left_value * 'value Eval.flagged_value
val value_assigned : ('loc, 'value) Eval.assigned -> 'value or_bottom
type 'location logic_dependency = {
term : Cil_types.identified_term;
direct : bool;
location : 'location option;
}
type 'location logic_assign =
Assigns of Cil_types.identified_term *
'location Eval.logic_dependency list
| Allocates of Cil_types.identified_term
| Frees of Cil_types.identified_term
type ('loc, 'value) argument = {
formal : Cil_types.varinfo;
concrete : Cil_types.exp;
avalue : ('loc, 'value) Eval.assigned;
}
type call_site = Cil_types.kernel_function * Cil_types.kinstr
type callstack = Eval.call_site list
type ('loc, 'value) call = {
kf : Cil_types.kernel_function;
callstack : Eval.callstack;
arguments : ('loc, 'value) Eval.argument list;
rest : (Cil_types.exp * ('loc, 'value) Eval.assigned) list;
return : Cil_types.varinfo option;
}
type recursion = {
depth : int;
substitution : (Cil_types.varinfo * Cil_types.varinfo) list;
base_substitution : Base.substitution;
withdrawal : Cil_types.varinfo list;
base_withdrawal : Base.Hptset.t;
}
type cacheable = Cacheable | NoCache | NoCacheCallers
end