Module Wp.Clabels

module Clabels: sig .. end


Normalized C-labels

Structural representation of logic labels. Compatible with pervasives comparison and structural equality.
type c_label = 
| Here
| Init
| Pre
| Post
| Exit
| At of string list * int (*
Label name, stmt-id.
*)
| CallAt of int (*
stmt-id
*)
| LabelParam of string (*
Logic label name in user-defined function or predicate
*)
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 loop_head_label : Cil_types.stmt -> Cil_types.logic_label
Returns a label that represent the first point of a loop body.
val mk_logic_label : Cil_types.stmt -> Cil_types.logic_label
create a virtual label to a statement (it can have no label)
val mk_stmt_label : Cil_types.stmt -> c_label
val mk_loop_label : Cil_types.stmt -> c_label
val c_label : Cil_types.logic_label -> c_label
Assumes the logic label only comes from normalized labels.

This is the case inside Wp module, where all ACSL formula comes from WpAnnot, which in turns always preprocess the labels through NormAtLabels.

val pretty : Format.formatter -> c_label -> unit
val lookup_name : c_label -> string
val lookup : (Cil_types.logic_label * Cil_types.logic_label) list ->
string -> c_label
lookup bindings lparam retrieves the actual label for the label in bindings for label parameter lparam.