sig
val register_ignore_pure_exp_hook :
(string -> Cil_types.exp -> unit) -> unit
val register_implicit_prototype_hook : (Cil_types.varinfo -> unit) -> unit
val register_incompatible_decl_hook :
(Cil_types.varinfo -> Cil_types.varinfo -> string -> unit) -> unit
val register_different_decl_hook :
(Cil_types.varinfo -> Cil_types.varinfo -> unit) -> unit
val register_new_global_hook : (Cil_types.varinfo -> bool -> unit) -> unit
val register_local_func_hook : (Cil_types.varinfo -> unit) -> unit
val register_ignore_side_effect_hook :
(Cabs.expression -> Cil_types.exp -> unit) -> unit
val register_conditional_side_effect_hook :
(Cabs.expression -> Cabs.expression -> unit) -> unit
val register_for_loop_all_hook :
(Cabs.for_clause ->
Cabs.expression -> Cabs.expression -> Cabs.statement -> unit) ->
unit
val register_for_loop_init_hook : (Cabs.for_clause -> unit) -> unit
val register_for_loop_test_hook : (Cabs.expression -> unit) -> unit
val register_for_loop_body_hook : (Cabs.statement -> unit) -> unit
val register_for_loop_incr_hook : (Cabs.expression -> unit) -> unit
val convFile : Cabs.file -> Cil_types.file
val frama_c_keep_block : string
val frama_c_destructor : string
val typeForInsertedVar : (Cil_types.typ -> Cil_types.typ) Pervasives.ref
val typeForInsertedCast :
(Cil_types.exp -> Cil_types.typ -> Cil_types.typ -> Cil_types.typ)
Pervasives.ref
val fresh_global : string -> string
val prefix : string -> string -> bool
val anonCompFieldName : string
val find_field_offset :
(Cil_types.fieldinfo -> bool) ->
Cil_types.fieldinfo list -> Cil_types.offset
val logicConditionalConversion :
Cil_types.typ -> Cil_types.typ -> Cil_types.typ
val arithmeticConversion : Cil_types.typ -> Cil_types.typ -> Cil_types.typ
val integralPromotion : Cil_types.typ -> Cil_types.typ
type local_env = private {
authorized_reads : Cil_datatype.Lval.Set.t;
known_behaviors : string list;
is_ghost : bool;
}
val empty_local_env : Cabs2cil.local_env
val ghost_local_env : bool -> Cabs2cil.local_env
val blockInitializer :
Cabs2cil.local_env ->
Cil_types.varinfo ->
Cabs.init_expression -> Cil_types.block * Cil_types.init * Cil_types.typ
val blockInit :
ghost:bool ->
Cil_types.lval -> Cil_types.init -> Cil_types.typ -> Cil_types.block
val mkAddrOfAndMark : Cil_types.location -> Cil_types.lval -> Cil_types.exp
val setDoTransformWhile : unit -> unit
val setDoAlternateConditional : unit -> unit
val integral_cast : Cil_types.typ -> Cil_types.term -> Cil_types.term
val allow_return_collapse : tlv:Cil_types.typ -> tf:Cil_types.typ -> bool
val compatibleTypes : Cil_types.typ -> Cil_types.typ -> Cil_types.typ
val areCompatibleTypes : Cil_types.typ -> Cil_types.typ -> bool
val stmtFallsThrough : Cil_types.stmt -> bool
end