Module `Slicing.SlicingCmds`Source

Source

type set =
  SlicingTypes.Fct_user_crit.t Frama_c_kernel.Cil_datatype.Varinfo.Map.t

Source

val get_select_kf : 
  SlicingTypes.sl_select ->
  Frama_c_kernel.Cil_types.kernel_function

Sourceval topologic_propagation : unit -> unit

Source

val select_pdg_nodes : 
  set ->
  SlicingTypes.sl_mark ->
  Pdg_types.PdgTypes.Node.t list ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

Source

val select_stmt : 
  set ->
  spare:bool ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

Source

val select_func_calls_to : 
  set ->
  spare:bool ->
  Frama_c_kernel.Kernel_function.t ->
  set

Source

val select_func_calls_into : 
  set ->
  spare:bool ->
  Frama_c_kernel.Kernel_function.t ->
  set

Source

val select_func_zone : 
  set ->
  SlicingTypes.sl_mark ->
  Frama_c_kernel.Locations.Zone.t ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

Source

val select_func_return : 
  set ->
  spare:bool ->
  Frama_c_kernel.Kernel_function.t ->
  set

Source

val select_stmt_ctrl : 
  set ->
  spare:bool ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

Source

val select_stmt_zone : 
  set ->
  SlicingTypes.sl_mark ->
  Frama_c_kernel.Locations.Zone.t ->
  before:bool ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

Source

val select_stmt_lval : 
  set ->
  SlicingTypes.sl_mark ->
  Frama_c_kernel.Datatype.String.Set.t ->
  before:bool ->
  Frama_c_kernel.Cil_types.stmt ->
  eval:Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

Source

val select_stmt_lval_rw : 
  set ->
  SlicingTypes.sl_mark ->
  rd:Frama_c_kernel.Datatype.String.Set.t ->
  wr:Frama_c_kernel.Datatype.String.Set.t ->
  Frama_c_kernel.Cil_types.stmt ->
  eval:Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Kernel_function.t ->
  set

Source

val select_stmt_pred : 
  set ->
  SlicingTypes.sl_mark ->
  Frama_c_kernel.Cil_types.predicate ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

Source

val select_stmt_term : 
  set ->
  SlicingTypes.sl_mark ->
  Frama_c_kernel.Cil_types.term ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

Source

val select_stmt_annot : 
  set ->
  SlicingTypes.sl_mark ->
  spare:bool ->
  Frama_c_kernel.Cil_types.code_annotation ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

Source

val select_stmt_annots : 
  set ->
  SlicingTypes.sl_mark ->
  spare:bool ->
  threat:bool ->
  user_assert:bool ->
  slicing_pragma:bool ->
  loop_inv:bool ->
  loop_var:bool ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

Source

val select_func_annots : 
  set ->
  SlicingTypes.sl_mark ->
  spare:bool ->
  threat:bool ->
  user_assert:bool ->
  slicing_pragma:bool ->
  loop_inv:bool ->
  loop_var:bool ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

Source

val select_func_lval : 
  set ->
  SlicingTypes.sl_mark ->
  Frama_c_kernel.Datatype.String.Set.t ->
  Frama_c_kernel.Kernel_function.t ->
  set

Source

val select_func_lval_rw : 
  set ->
  SlicingTypes.sl_mark ->
  rd:Frama_c_kernel.Datatype.String.Set.t ->
  wr:Frama_c_kernel.Datatype.String.Set.t ->
  eval:Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Kernel_function.t ->
  set

Sourceval add_selection : set -> unit

Sourceval add_persistent_selection : set -> unit

Sourceval add_persistent_cmdline : unit -> unit

Sourceval apply_all : propagate_to_callers:bool -> unit

Sourceval apply_all_actions : unit -> unit

Sourceval apply_next_action : unit -> unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-slicing.core/Slicing/SlicingCmds/index.html

Module `Slicing.SlicingCmds`Source

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-slicing.core/Slicing/SlicingCmds/index.html

Module Slicing.SlicingCmdsSource

Module `Slicing.SlicingCmds`Source