package frama-c

  1. Overview
  2. Docs

Module Slicing.SlicingMarksSource

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

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.

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
Sourceval missing_input_mark : call:SlicingTypes.sl_mark -> called:SlicingTypes.sl_mark -> SlicingTypes.sl_mark option
Sourceval missing_output_mark : call:SlicingTypes.sl_mark -> called:SlicingTypes.sl_mark -> SlicingTypes.sl_mark option
Sourceval empty_sig : sig_marks
Sourceval get_input_mark : sig_marks -> int -> SlicingTypes.sl_mark
Sourceval merge_inputs_m1_mark : sig_marks -> 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