package frama-c

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val print_select : Format.formatter -> SlicingTypes.sl_select -> unit
val bottom_msg : Frama_c_kernel.Kernel_function.t -> unit

this one is similar to select_stmt_zone with the return statement * when the function is defined, but it can also be used for undefined functions.

marking a call node means that a choose_call will have to decide that to * call according to the slicing-level, but anyway, the call will be visible.

module Selections : sig ... end
val call_ff_in_caller : caller:SlicingInternals.fct_slice -> to_call:SlicingInternals.fct_slice -> unit

change the call to call the given slice. * This is a user request, so it might be the case that * the new function doesn't compute enough outputs : * in that case, add outputs first.

val call_fsrc_in_caller : caller:SlicingInternals.fct_slice -> to_call:Frama_c_kernel.Kernel_function.t -> unit
val call_min_f_in_caller : caller:SlicingInternals.fct_slice -> to_call:Frama_c_kernel.Cil_types.kernel_function -> unit
val is_already_selected : SlicingInternals.fct_slice -> SlicingTypes.sl_select -> bool
val add_ff_selection : SlicingInternals.fct_slice -> SlicingTypes.sl_select -> unit
val add_fi_selection : SlicingTypes.sl_select -> unit

add a persistent selection to the function. * This might change its slicing level in order to call slices later on.

OCaml

Innovation. Community. Security.