package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c-slicing.core/Slicing/Api/Select/index.html

Module `Api.Select`Source

Slicing selections.

Sourcetype t = SlicingTypes.sl_select

Internal selection.

Sourceval dyn_t : t Frama_c_kernel.Type.t

For dynamic type checking.

Sourcetype set = SlicingCmds.set

Set of colored selections.

Sourceval dyn_set : set Frama_c_kernel.Type.t

For dynamic type checking.

Selectors.

Sourceval empty_selects : set

Empty selection.

Statement selectors.

Source

val select_stmt : 
  set ->
  spare:bool ->
  Frama_c_kernel.Cil_datatype.Stmt.t ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

To select a statement.

Source

val select_stmt_ctrl : 
  set ->
  spare:bool ->
  Frama_c_kernel.Cil_datatype.Stmt.t ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

To select a statement reachability. Note: add also a transparent selection on the whole statement.

Source

val select_stmt_lval_rw : 
  set ->
  Mark.t ->
  rd:Frama_c_kernel.Datatype.String.Set.t ->
  wr:Frama_c_kernel.Datatype.String.Set.t ->
  Frama_c_kernel.Cil_datatype.Stmt.t ->
  eval:Frama_c_kernel.Cil_datatype.Stmt.t ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

To select rw accesses to lvalues (given as string) related to a statement. Variables of ~rd and ~wr string are bounded relatively to the whole scope of the function. The interpretation of the address of the lvalues is done just before the execution of the statement ~eval. The selection preserve the ~rd and ~wr accesses contained into the statement ki. Note: add also a transparent selection on the whole statement.

Source

val select_stmt_lval : 
  set ->
  Mark.t ->
  Frama_c_kernel.Datatype.String.Set.t ->
  before:bool ->
  Frama_c_kernel.Cil_datatype.Stmt.t ->
  eval:Frama_c_kernel.Cil_datatype.Stmt.t ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

To select lvalues (given as string) related to a statement. Variables of lval_str string are bounded relatively to the whole scope of the function. The interpretation of the address of the lvalue is done just before the execution of the statement ~eval. The selection preserve the value of these lvalues before or after (c.f. boolean ~before) the statement ki. Note: add also a transparent selection on the whole statement.

Source

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

To select a zone value related to a statement. Note: add also a transparent selection on the whole statement.

Source

val select_stmt_term : 
  set ->
  Mark.t ->
  Frama_c_kernel.Cil_types.term ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

To select a predicate value related to a statement. Note: add also a transparent selection on the whole statement.

Source

val select_stmt_pred : 
  set ->
  Mark.t ->
  Frama_c_kernel.Cil_types.predicate ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

To select a predicate value related to a statement. Note: add also a transparent selection on the whole statement.

Source

val select_stmt_annot : 
  set ->
  Mark.t ->
  spare:bool ->
  Frama_c_kernel.Cil_types.code_annotation ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

To select the annotations related to a statement. Note: add also a transparent selection on the whole statement.

Source

val select_stmt_annots : 
  set ->
  Mark.t ->
  spare:bool ->
  threat:bool ->
  user_assert:bool ->
  slicing_annot:bool ->
  loop_inv:bool ->
  loop_var:bool ->
  Frama_c_kernel.Cil_datatype.Stmt.t ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

To select the annotations related to a statement. Note: add also a transparent selection on the whole statement.

Function selectors.

Source

val select_func_lval_rw : 
  set ->
  Mark.t ->
  rd:Frama_c_kernel.Datatype.String.Set.t ->
  wr:Frama_c_kernel.Datatype.String.Set.t ->
  eval:Frama_c_kernel.Cil_datatype.Stmt.t ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

To select rw accesses to lvalues (given as a string) related to a function. Variables of ~rd and ~wr string are bounded relatively to the whole scope of the function. The interpretation of the address of the lvalues is done just before the execution of the statement ~eval. The selection preserve the value of these lvalues into the whole project.

Source

val select_func_lval : 
  set ->
  Mark.t ->
  Frama_c_kernel.Datatype.String.Set.t ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

To select lvalues (given as a string) related to a function. Variables of lval_str string are bounded relatively to the scope of the first statement of kf. The interpretation of the address of the lvalues is done just before the execution of the first statement kf. The selection preserve the value of these lvalues before execution of the return statement.

Source

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

To select an output zone related to a function.

Source

val select_func_return : 
  set ->
  spare:bool ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

To select the function result (returned value).

Source

val select_func_calls_to : 
  set ->
  spare:bool ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

To select every calls to the given function, i.e. the call keeps its semantics in the slice.

Source

val select_func_calls_into : 
  set ->
  spare:bool ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

To select every calls to the given function without the selection of its inputs/outputs.

Source

val select_func_annots : 
  set ->
  Mark.t ->
  spare:bool ->
  threat:bool ->
  user_assert:bool ->
  slicing_annot:bool ->
  loop_inv:bool ->
  loop_var:bool ->
  Frama_c_kernel.Cil_types.kernel_function ->
  set

To select the annotations related to a function.

Pdg selectors.

Source

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

Internal use only

Sourceval get_function : t -> Frama_c_kernel.Cil_types.kernel_function

The function related to an internal selection.

Sourceval merge_internal : t -> t -> t

The function related to an internal selection.

Sourceval add_to_selects_internal : t -> set -> set

Sourceval iter_selects_internal : (t -> unit) -> set -> unit

Sourceval fold_selects_internal : ('a -> t -> 'a) -> 'a -> set -> 'a

Source

val select_stmt_internal : 
  Frama_c_kernel.Cil_types.kernel_function ->
  ?select:t ->
  Frama_c_kernel.Cil_types.stmt ->
  Mark.t ->
  t

Internally used to select a statement :

if is_ctrl_mark m, propagate ctrl_mark on ctrl dependencies of the statement
if is_addr_mark m, propagate addr_mark on addr dependencies of the statement
if is_data_mark m, propagate data_mark on data dependencies of the statement Marks the node with a spare_mark and propagate so that the dependencies that were not selected yet will be marked spare. When the statement is a call, its functional inputs/outputs are also selected (The call is still selected even it has no output). When the statement is a composed one (block, if, etc...), all the sub-statements are selected.

raises SlicingTypes.NoPdg
when the Pdg cannot be computed.

Source

val select_label_internal : 
  Frama_c_kernel.Cil_types.kernel_function ->
  ?select:t ->
  Frama_c_kernel.Cil_types.logic_label ->
  Mark.t ->
  t

Source

val select_min_call_internal : 
  Frama_c_kernel.Cil_types.kernel_function ->
  ?select:t ->
  Frama_c_kernel.Cil_types.stmt ->
  Mark.t ->
  t

Internally used to select a statement call without its inputs/outputs so that it doesn't select the statements computing the inputs of the called function as select_stmt_internal would do. Raise Invalid_argument when the stmt isn't a call.

raises SlicingTypes.NoPdg
when the Pdg cannot be computed.

Source

val select_stmt_zone_internal : 
  Frama_c_kernel.Cil_types.kernel_function ->
  ?select:t ->
  Frama_c_kernel.Cil_types.stmt ->
  before:bool ->
  Frama_c_kernel.Locations.Zone.t ->
  Mark.t ->
  t

Internally used to select a zone value at a program point.

raises SlicingTypes.NoPdg
when the Pdg cannot be computed.

Source

val select_zone_at_entry_point_internal : 
  Frama_c_kernel.Cil_types.kernel_function ->
  ?select:t ->
  Frama_c_kernel.Locations.Zone.t ->
  Mark.t ->
  t

Internally used to select a zone value at the beginning of a function. For a defined function, it is similar to select_stmt_zone_internal with the initial statement, but it can also be used for undefined functions.

raises SlicingTypes.NoPdg
when the Pdg cannot be computed.

Source

val select_zone_at_end_internal : 
  Frama_c_kernel.Cil_types.kernel_function ->
  ?select:t ->
  Frama_c_kernel.Locations.Zone.t ->
  Mark.t ->
  t

Internally used to select a zone value at the end of a function. For a defined function, it is similar to select_stmt_zone_internal with the return statement, but it can also be used for undefined functions.

raises SlicingTypes.NoPdg
when the Pdg cannot be computed.

Source

val select_modified_output_zone_internal : 
  Frama_c_kernel.Cil_types.kernel_function ->
  ?select:t ->
  Frama_c_kernel.Locations.Zone.t ->
  Mark.t ->
  t

Internally used to select the statements that modify the given zone considered as in output. Be careful that it is NOT the same as selecting the zone at the end! The 'undef' zone is not propagated...

raises SlicingTypes.NoPdg
when the Pdg cannot be computed.

Source

val select_stmt_ctrl_internal : 
  Frama_c_kernel.Cil_types.kernel_function ->
  ?select:t ->
  Frama_c_kernel.Cil_types.stmt ->
  t

Internally used to select a statement reachability : Only propagate a ctrl_mark on the statement control dependencies.

raises SlicingTypes.NoPdg
when the Pdg cannot be computed.

Source

val select_entry_point_internal : 
  Frama_c_kernel.Cil_types.kernel_function ->
  ?select:t ->
  Mark.t ->
  t

Source

val select_return_internal : 
  Frama_c_kernel.Cil_types.kernel_function ->
  ?select:t ->
  Mark.t ->
  t

Source

val select_decl_var_internal : 
  Frama_c_kernel.Cil_types.kernel_function ->
  ?select:t ->
  Frama_c_kernel.Cil_types.varinfo ->
  Mark.t ->
  t

Source

val select_pdg_nodes_internal : 
  Frama_c_kernel.Cil_types.kernel_function ->
  ?select:t ->
  Pdg_types.PdgTypes.Node.t list ->
  Mark.t ->
  t

Internally used to select PDG nodes :

if is_ctrl_mark m, propagate ctrl_mark on ctrl dependencies of the statement
if is_addr_mark m, propagate addr_mark on addr dependencies of the statement
if is_data_mark m, propagate data_mark on data dependencies of the statement Marks the node with a spare_mark and propagate so that the dependencies that were not selected yet will be marked spare.

Debug

Sourceval pretty : Stdlib.Format.formatter -> t -> unit

On This Page

Slicing selections.
1. Selectors.
2. Debug

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-slicing.core/Slicing/Api/Select/index.html

Module Api.SelectSource

Slicing selections.

Selectors.

Statement selectors.

Function selectors.

Pdg selectors.

Internal use only

Debug

Module `Api.Select`Source