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.

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.

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.

val register_new_global_hook : (Cil_types.varinfo -> bool -> unit) -> unit

Hook called when a new global is created. The varinfo vi is the one corresponding to the global, while the boolean is true iff vi was already existing (it is false if this is the first declaration/definition of vi in the file).

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.

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)

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.

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.

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.

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.

val convFile : Cabs.file -> Cil_types.file
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 frama_c_destructor : string

Name of the attribute used to store the function that should be called when the corresponding variable exits its scope.

val fc_local_static : string

Name of the attribute used to indicate that a given static variable has a local syntactic scope (despite a global lifetime).

val typeForInsertedVar : (Cil_types.typ -> Cil_types.typ) Stdlib.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) Stdlib.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.

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

*)
   is_paren : bool; (*

is the current expr a child of A.PAREN

*)
   inner_paren : bool; (*

used internally for normalizations of unop and binop.

*)
}

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 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.

val areCompatibleTypes : Cil_types.typ -> Cil_types.typ -> bool

areCompatibleTypes ot nt checks that the two given types are compatible (C99, 6.2.7). Note however that we use a slightly relaxed notion of compatibility to cope with de-facto usages. In particular, this function is *not* symmetric: in some cases, when objects of type ot can safely be converted to objects of type nt, we accept them as compatible to avoid spurious casts.

val stmtFallsThrough : Cil_types.stmt -> bool

returns true if the given statement can fall through the next syntactical one.