Module `Slicing.SlicingMarks`Source

Sourceval bottom_mark : SlicingTypes.sl_mark

Sourceval mk_user_mark : data:bool -> addr:bool -> ctrl:bool -> SlicingTypes.sl_mark

Sourceval mk_gen_spare : SlicingTypes.sl_mark

generated spare = the smallest visible mark

Sourceval mk_user_spare : SlicingTypes.sl_mark

Sourceval is_bottom_mark : SlicingTypes.sl_mark -> bool

Sourceval is_top_mark : SlicingTypes.sl_mark -> bool

Sourceval is_spare_mark : SlicingTypes.sl_mark -> bool

Sourceval is_ctrl_mark : SlicingTypes.sl_mark -> bool

Sourceval is_addr_mark : SlicingTypes.sl_mark -> bool

Sourceval is_data_mark : SlicingTypes.sl_mark -> bool

Sourceval merge_marks : SlicingTypes.sl_mark list -> SlicingTypes.sl_mark

Sourceval inter_marks : SlicingTypes.sl_mark list -> SlicingTypes.sl_mark

Source

val combine_marks : 
  SlicingTypes.sl_mark ->
  SlicingTypes.sl_mark ->
  SlicingTypes.sl_mark * SlicingTypes.sl_mark

combine_marks add a new information to the old value.

returns
(new_mark, is_new) where is_new=true if the new mark is not included in the old one.

Source

val minus_marks : 
  SlicingTypes.sl_mark ->
  SlicingTypes.sl_mark ->
  SlicingTypes.sl_mark

Sourceval compare_marks : SlicingTypes.sl_mark -> SlicingTypes.sl_mark -> int

Sourceval mark_to_string : SlicingTypes.sl_mark -> string

Sourceval pretty_mark : Format.formatter -> SlicingTypes.sl_mark -> unit

Source

val missing_input_mark : 
  call:SlicingTypes.sl_mark ->
  called:SlicingTypes.sl_mark ->
  SlicingTypes.sl_mark option

Source

val missing_output_mark : 
  call:SlicingTypes.sl_mark ->
  called:SlicingTypes.sl_mark ->
  SlicingTypes.sl_mark option

Sourcetype sig_marks = SlicingTypes.sl_mark Pdg_types.PdgIndex.Signature.t

Sourceval empty_sig : sig_marks

Sourceval get_input_mark : sig_marks -> int -> SlicingTypes.sl_mark

Source

val get_all_input_marks : 
  sig_marks ->
  (Pdg_types.PdgIndex.Signature.in_key * SlicingTypes.sl_mark) list

Source

val get_matching_input_marks : 
  sig_marks ->
  Frama_c_kernel.Locations.Zone.t ->
  (Pdg_types.PdgIndex.Signature.in_key * SlicingTypes.sl_mark) list

Sourceval merge_inputs_m1_mark : sig_marks -> SlicingTypes.sl_mark

Source

val get_input_loc_under_mark : 
  sig_marks ->
  Frama_c_kernel.Locations.Zone.t ->
  SlicingTypes.sl_mark

Sourceval get_in_ctrl_mark : sig_marks -> SlicingTypes.sl_mark

Sourceval something_visible : sig_marks -> bool

Sourceval some_visible_out : sig_marks -> bool

Sourceval is_topin_visible : sig_marks -> bool

Sourceval get_marked_out_zone : sig_marks -> bool * Frama_c_kernel.Locations.Zone.t

Sourceval pretty_sig : Format.formatter -> sig_marks -> unit

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Slicing.SlicingMarks`Source

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module Slicing.SlicingMarksSource

Module `Slicing.SlicingMarks`Source