Frama-C:
Plug-ins:
Libraries:

Frama-C API - Info

exception EraseAssigns

exception that fun_assign_visible should raise to indicate that the corresponding assigns clause should be erased entirely

exception EraseAllocation

exception that fun_frees_visible or fun_allocates_visible should raise to indicate that the corresponding allocation clause should be erased entirely

type proj

some type for the whole project information

type fct

some type for a function information

val fct_info : proj -> Cil_types.kernel_function -> fct list

This function will be called for each function of the source program. A new function will be created for each element of the returned list.

val fct_name : Cil_types.varinfo -> fct -> string

useful when we want to have several functions in the result for one source function. If it is not the case, you can return varinfo.vname. It is the responsibility of the user to given different names to different function.

val param_visible : fct -> int -> bool

tells if the n-th formal parameter is visible.

val body_visible : fct -> bool

tells if the body of a function definition is visible. True is most cases, but can be defined to be false when we want to export only the declaration of a function instead of its definition

val loc_var_visible : fct -> Cil_types.varinfo -> bool

tells if the local variable is visible.

val inst_visible : fct -> Cil_types.stmt -> bool

tells if the statement is visible.

val label_visible : fct -> Cil_types.stmt -> Cil_types.label -> bool

tells if the label is visible.

val annotation_visible : fct -> Cil_types.stmt -> Cil_types.code_annotation -> bool

tells if the annotation, attached to the given statement is visible.

val fun_precond_visible : fct -> Cil_types.predicate -> bool
val fun_postcond_visible : fct -> Cil_types.predicate -> bool
val fun_variant_visible : fct -> Cil_types.term -> bool
val fun_frees_visible : fct -> Cil_types.identified_term -> bool
val fun_allocates_visible : fct -> Cil_types.identified_term -> bool
val fun_assign_visible : fct -> Cil_types.from -> bool

true if the assigned value (first component of the from) is visible

  • raises EraseAssigns

    to indicate that the corresponding assigns clause should be erased entirely (i.e. assigns everything. If it were to just return false to all elements, this would result in assigns \nothing

val fun_deps_visible : fct -> Cil_types.identified_term -> bool

true if the corresponding functional dependency is visible.

val called_info : (proj * fct) -> Cil_types.stmt -> (Cil_types.kernel_function * fct) option

called_info will be called only if the call statement is visible. If it returns None, the source call will be visible, else it will use the returned fct to know if the return value and the arguments are visible. The input fct parameter is the one of the caller function.

val res_call_visible : fct -> Cil_types.stmt -> bool

tells if the lvalue of the call has to be visible

val result_visible : Cil_types.kernel_function -> fct -> bool

tells if the function returns something or if the result is void. Notice that if this function returns true the function will have the same return type than the original function. So, if it was already void, it makes no difference if this function returns true or false.

  • For a defined function, this should give the same result than inst_visible fct_info (Kernel_function.find_return kf).
  • res_call_visible must return false if result_visible returns false on the called function.
val cond_edge_visible : fct -> Cil_types.stmt -> bool * bool

cond_edge_visible f s implies that s is an 'if' in f. The first returned boolean indicates that the 'then' edge is useful, the second one the 'else' is. Setting one or both to true will lead to the simplification in the 'if'.