val is_ignorable_type : Cil.typ -> boolval is_ignorable : (Cil.varinfo * 'a) option -> boolmodule LSSet : sig ... endval init : Cil.file -> unitval remove_idx : Cil.offset -> offsval d_offs : unit -> offs -> Pretty.docval d_acct :
unit ->
[< `Struct of Cil.compinfo * offs | `Type of Cil.typ ] ->
Pretty.docval d_memo :
unit ->
([< `Struct of Cil.compinfo * offs | `Type of Cil.typ ]
* (Cil.varinfo * offs) option) ->
Pretty.docval get_type : Cil.typ -> Cil.exp -> acc_typtype var_o = Cil.varinfo optiontype off_o = Cil.offset optionval add_one :
Cil.exp ->
bool ->
int ->
acc_typ ->
(Cil.varinfo * offs) option ->
part ->
unitval type_from_type_offset : acc_typ -> Cil.typval add_struct :
Cil.exp ->
bool ->
int ->
acc_typ ->
(Cil.varinfo * offs) option ->
part ->
unitval add_propagate : Cil.exp -> bool -> int -> acc_typ -> 'a -> part -> unitval distribute_access_lval :
(bool -> bool -> 'a -> Cil.exp -> 'b) ->
bool ->
bool ->
'a ->
Cil.lval ->
unitval distribute_access_lval_addr :
(bool -> bool -> 'a -> Cil.exp -> 'b) ->
bool ->
bool ->
'a ->
Cil.lval ->
unitval distribute_access_offset :
(bool -> bool -> 'a -> Cil.exp -> 'b) ->
'a ->
Cil.offset ->
unitval distribute_access_exp :
(bool -> bool -> 'a -> Cil.exp -> 'b) ->
bool ->
bool ->
'a ->
Cil.exp ->
unitval only_read : 'a -> (('b * bool * 'c * 'd * 'e) Batteries.Set.t * 'f) -> boolval common_resource : 'a -> ('b * LSSet.t) -> boolval bot_partition : 'a option -> 'b -> boolval check_accs :
('a option * LSSet.t * bool) ->
('a * bool * 'b * 'c * LSSet.t) ->
'a option * LSSet.t * boolval check_safe :
'a option ->
(('b * bool * 'c * 'd * LSSet.t) Batteries.Set.t * 'e) ->
'b option ->
'b optionval is_all_safe : unit -> boolval print_summary : unit -> unitval print_accesses : unit -> unitval print_result : unit -> unit