Module Clabels

module Clabels: sig .. end

Normalized C-labels

type c_label =

`\|`	`Here`
`\|`	`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 : 'a -> 'a -> bool

module T: sig .. end

module LabelMap: FCMap.Make(T)

module LabelSet: FCSet.Make(T)

val has_prefix : string -> string -> bool

val names_at : Cil_types.label list -> string list

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 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 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.