Module Wp.ClabelsSource

Normalized C-labels

Structural representation of logic labels. Compatible with stdlib comparison and structural equality.

Sourcetype c_label
Sourceval is_here : c_label -> bool
Sourceval mem : c_label -> c_label list -> bool
Sourceval equal : c_label -> c_label -> bool
Sourcemodule T : sig ... end
Sourcemodule LabelMap : Map.S with type key = c_label
Sourcemodule LabelSet : Set.S with type elt = c_label
Sourceval pre : c_label
Sourceval here : c_label
Sourceval next : c_label
Sourceval init : c_label
Sourceval post : c_label
Sourceval exit : c_label
Sourceval break : c_label
Sourceval continue : c_label
Sourceval default : c_label
Sourceval loopentry : c_label
Sourceval loopcurrent : c_label
Sourceval formal : string -> c_label
Sourceval case : int64 -> c_label
Sourceval stmt_post : Frama_c_kernel.Cil_types.stmt -> c_label
Sourceval loop_entry : Frama_c_kernel.Cil_types.stmt -> c_label

Assumes the logic label only comes from normalized or non-ambiguous labels. Ambiguous labels are: Old, LoopEntry and LoopCurrent, since they points to different program points dependending on the context.

Sourceval is_post : Frama_c_kernel.Cil_types.logic_label -> bool

Checks whether the logic-label is Post or to_logic post

Sourceval pretty : Format.formatter -> c_label -> unit

lookup bindings lparam retrieves the actual label for the label in bindings for label parameter lparam.