package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
val print_select : Stdlib.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.

val select_zone_at_entry : Frama_c_kernel.Kernel_function.t -> ?select:SlicingTypes.sl_select -> Frama_c_kernel.Locations.Zone.t -> SlicingTypes.sl_mark -> SlicingTypes.sl_select

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.

val select_entry_point : Frama_c_kernel.Kernel_function.t -> ?select:SlicingTypes.sl_select -> SlicingTypes.sl_mark -> SlicingTypes.sl_select
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.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct