module Cabs2cil:sig
..end
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_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
(x && (y||z++))
,
we have a warning on z++
, not on y||z++
, and similarly, on
(x && (y++||z))
, we only have a warning on y++
).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 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
typeForInsertedVar
, but for casts.
typeForInsertedCast expr original_type destination_type
returns the type into which expr
, which has type original_type
and
whose type must be converted into destination_type
, must be casted.
By default, returns destination_type
.
This applies only to implicit casts. Casts already present
in the source code are exempt from this hook.
val fresh_global : string -> string
fresh_global prefix
creates a variable name not clashing with any other
globals and starting with prefix
val prefix : string -> string -> bool
s
starts with the prefix p
.val anonCompFieldName : string
val find_field_offset : (Cil_types.fieldinfo -> bool) -> Cil_types.fieldinfo list -> Cil_types.offset
Not_found
if no such field exists.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 {
|
: |
(* | sets of lvalues that can be read regardless of a potential write access between sequence points. Mainly for tmp variables introduced by the normalization. | *) |
|
known_behaviors : |
(* | list of known behaviors at current point. | *) |
|
is_ghost : |
(* | whether we're analyzing ghost code or not | *) |
val empty_local_env : local_env
val ghost_local_env : bool -> local_env
empty_local_env
, but sets the ghost status to the value of its
argumentval blockInitializer : 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
init
applied to lvalue lval
of type typ
.val mkAddrOfAndMark : Cil_types.location -> Cil_types.lval -> Cil_types.exp
mkAddrOf
after marking variable whose address is taken.val setDoTransformWhile : unit -> unit
continue
in while loops get transformed
into forward gotos, like it is already done in do-while and for loops.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
lv = f()
, if tf
is the return type of f
and tlv
the type of lv
, allow_return_collapse ~tlv ~tf
returns false
if a temporary must be introduced to hold the result of f
, and
true otherwise.
Currently, implicit cast between pointers or cast from an scalar type
or a strictly bigger one are accepted without cast. This is subject
to change without notice.
Since Oxygen-20120901
val compatibleTypes : Cil_types.typ -> Cil_types.typ -> Cil_types.typ
Failure
with an explanation
if the two types are not compatibleval compatibleTypesp : Cil_types.typ -> Cil_types.typ -> bool