Slicing.SlicingMarksval bottom_mark : SlicingTypes.sl_markval mk_user_mark : data:bool -> addr:bool -> ctrl:bool -> SlicingTypes.sl_markval mk_gen_spare : SlicingTypes.sl_markgenerated spare = the smallest visible mark
val mk_user_spare : SlicingTypes.sl_markval is_bottom_mark : SlicingTypes.sl_mark -> boolval is_top_mark : SlicingTypes.sl_mark -> boolval is_spare_mark : SlicingTypes.sl_mark -> boolval is_ctrl_mark : SlicingTypes.sl_mark -> boolval is_addr_mark : SlicingTypes.sl_mark -> boolval is_data_mark : SlicingTypes.sl_mark -> boolval merge_marks : SlicingTypes.sl_mark list -> SlicingTypes.sl_markval inter_marks : SlicingTypes.sl_mark list -> SlicingTypes.sl_markval combine_marks :
SlicingTypes.sl_mark ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_mark * SlicingTypes.sl_markcombine_marks add a new information to the old value.
val minus_marks :
SlicingTypes.sl_mark ->
SlicingTypes.sl_mark ->
SlicingTypes.sl_markval compare_marks : SlicingTypes.sl_mark -> SlicingTypes.sl_mark -> intval mark_to_string : SlicingTypes.sl_mark -> stringval pretty_mark : Stdlib.Format.formatter -> SlicingTypes.sl_mark -> unitval missing_input_mark :
call:SlicingTypes.sl_mark ->
called:SlicingTypes.sl_mark ->
SlicingTypes.sl_mark optionval missing_output_mark :
call:SlicingTypes.sl_mark ->
called:SlicingTypes.sl_mark ->
SlicingTypes.sl_mark optiontype sig_marks = SlicingTypes.sl_mark Pdg_types.PdgIndex.Signature.tval empty_sig : sig_marksval get_input_mark : sig_marks -> int -> SlicingTypes.sl_markval get_all_input_marks :
sig_marks ->
(Pdg_types.PdgIndex.Signature.in_key * SlicingTypes.sl_mark) listval get_matching_input_marks :
sig_marks ->
Frama_c_kernel.Locations.Zone.t ->
(Pdg_types.PdgIndex.Signature.in_key * SlicingTypes.sl_mark) listval merge_inputs_m1_mark : sig_marks -> SlicingTypes.sl_markval get_input_loc_under_mark :
sig_marks ->
Frama_c_kernel.Locations.Zone.t ->
SlicingTypes.sl_markval get_in_ctrl_mark : sig_marks -> SlicingTypes.sl_markval something_visible : sig_marks -> boolval some_visible_out : sig_marks -> boolval is_topin_visible : sig_marks -> boolval get_marked_out_zone : sig_marks -> bool * Frama_c_kernel.Locations.Zone.tval pretty_sig : Stdlib.Format.formatter -> sig_marks -> unit