Module Wp.Clabels

module Clabels: sig .. end


Normalized C-labels

Normalized C-labels

Structural representation of logic labels. Compatible with pervasives comparison and structural equality.
type c_label 
val is_here : c_label -> bool
val equal : c_label -> c_label -> bool
module T: sig .. end
module LabelMap: FCMap.S  with type key = c_label
module LabelSet: FCSet.S  with type elt = c_label
val pre : c_label
val here : c_label
val init : c_label
val post : c_label
val formal : string -> c_label
val stmt : Cil_types.stmt -> c_label
val loop_entry : Cil_types.stmt -> c_label
val loop_current : Cil_types.stmt -> c_label
val to_logic : c_label -> Cil_types.logic_label
val of_logic : Cil_types.logic_label -> 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.
val pretty : Format.formatter -> c_label -> unit
val name : Cil_types.logic_label -> string
val lookup : (Cil_types.logic_label * Cil_types.logic_label) list ->
string -> Cil_types.logic_label
lookup bindings lparam retrieves the actual label for the label in bindings for label parameter lparam.