Previous  Up  Next

Module Cabs2cil

module Cabs2cil: sig .. end
Registers a new hook that will be applied each time a side-effect free expression whose result is unused is dropped. The string is the name of the current function.
val register_ignore_pure_exp_hook : (string -> Cil_types.exp -> unit) -> unit
val register_implicit_prototype_hook : (Cil_types.varinfo -> unit) -> unit
new hook called when an implicit prototype is generated.
Since Carbon-20101201
val register_incompatible_decl_hook : (Cil_types.varinfo -> Cil_types.varinfo -> string -> unit) -> unit
new hook called when two conflicting declarations are found. The hook takes as argument the old and new varinfo, and a description of the issue.
Since Carbon-20101201
val register_different_decl_hook : (Cil_types.varinfo -> Cil_types.varinfo -> unit) -> unit
new hook called when a definition has a compatible but not strictly identical prototype than its declaration The hook takes as argument the old and new varinfo. Note that only the old varinfo is kept in the AST, and that its type will be modified in place just after to reflect the merge of the prototypes.
Since Carbon-20101201
val register_local_func_hook : (Cil_types.varinfo -> unit) -> unit
new hook called when encountering a definition of a local function. The hook take as argument the varinfo of the local function.
Since Carbon-20101201
val register_ignore_side_effect_hook : (Cabs.expression -> Cil_types.exp -> unit) -> unit
new hook called when side-effects are dropped. The first argument is the original expression, the second one the (side-effect free) normalized expression.
val register_conditional_side_effect_hook : (Cabs.expression -> Cabs.expression -> unit) -> unit
new hook called when an expression with side-effect is evaluated conditionally (RHS of && or ||, 2nd and 3rd term of ?:). Note that in case of nested conditionals, only the innermost expression with side-effects will trigger the hook (for instance, in (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
new hook that will be called when processing a for loop. Arguments are the four elements of the for clause (init, test, increment, body)
Since Oxygen-20120901
val register_for_loop_init_hook : (Cabs.for_clause -> unit) -> unit
new hook that will be called when processing a for loop. Argument is the initializer of the for loop.
Since Oxygen-20120901
val register_for_loop_test_hook : (Cabs.expression -> unit) -> unit
new hook that will be called when processing a for loop. Argument is the test of the loop.
Since Oxygen-20120901
val register_for_loop_body_hook : (Cabs.statement -> unit) -> unit
new hook that will called when processing a for loop. Argument is the body of the loop.
Since Oxygen-20120901
val register_for_loop_incr_hook : (Cabs.expression -> unit) -> unit
new hook that will be called when processing a for loop. Argument is the increment part of the loop.
Since Oxygen-20120901
val convFile : Cabs.file -> Cil_types.file
Consult the Plugin Development Guide for additional details.
val frama_c_keep_block : string
Name of the attribute inserted by the elaboration to prevent user blocks from disappearing. It can be removed whenever block contracts have been processed.
val typeForInsertedVar : (Cil_types.typ -> Cil_types.typ) Pervasives.ref
A hook into the code that creates temporary local vars. By default this is the identity function, but you can overwrite it if you need to change the types of cabs2cil-introduced temp variables.
val typeForInsertedCast : (Cil_types.exp -> Cil_types.typ -> Cil_types.typ -> Cil_types.typ)
       Pervasives.ref
Like 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
Check that s starts with the prefix p.
val anonCompFieldName : string
val find_field_offset : (Cil_types.fieldinfo -> bool) -> Cil_types.fieldinfo list -> Cil_types.offset
returns the offset (can be more than one field in case of unnamed members) corresponding to the first field matching the condition.
Raises Not_found if no such field exists.
val logicConditionalConversion : Cil_types.typ -> Cil_types.typ -> Cil_types.typ
returns the type of the result of a logic operator applied to values of the corresponding input types.
val arithmeticConversion : Cil_types.typ -> Cil_types.typ -> Cil_types.typ
Deprecated.Nitrogen-20111001 moved to Cil module
returns the type of the result of an arithmetic operator applied to values of the corresponding input types.
val integralPromotion : Cil_types.typ -> Cil_types.typ
Deprecated.Nitrogen-20111001 moved to Cil module.
performs the usual integral promotions mentioned in C reference manual.
type local_env = private {
   authorized_reads : Cil_datatype.Lval.Set.t; (*
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 : string list; (*
list of known behaviors at current point.
*)
   is_ghost : bool; (*
whether we're analyzing ghost code or not
*)
}
local information needed to typecheck expressions and statements
val empty_local_env : local_env
an empty local environment.
val ghost_local_env : bool -> local_env
same as empty_local_env, but sets the ghost status to the value of its argument
val 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
Returns a block of statements equivalent to the initialization init applied to lvalue lval of type typ.
val mkAddrOfAndMark : Cil_types.location -> Cil_types.lval -> Cil_types.exp
Applies mkAddrOf after marking variable whose address is taken.
val setDoTransformWhile : unit -> unit
If called, sets a flag so that continue in while loops get transformed into forward gotos, like it is already done in do-while and for loops.
val setDoAlternateConditional : unit -> unit
If called, sets a flag so that translation of conditionals does not result in forward ingoing gotos (from the if-branch to the else-branch).
val integral_cast : Cil_types.typ -> Cil_types.term -> Cil_types.term
Raise Failure
val allow_return_collapse : tlv:Cil_types.typ -> tf:Cil_types.typ -> bool
Given a call 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
Check that the two given types are compatible (C99, 6.2.7), and return their composite type. Raise Failure with an explanation if the two types are not compatible
Since Oxygen-20120901
val compatibleTypesp : Cil_types.typ -> Cil_types.typ -> bool
Check that the two given types are compatible (C99, 6.2.7), and return a boolean.
Since Neon-20140301