module Clabels:sig
..end
type
c_label =
| |
Here |
|||
| |
Init |
|||
| |
Pre |
|||
| |
Post |
|||
| |
Exit |
|||
| |
At of |
(* |
Label name, stmt-id.
| *) |
| |
CallAt of |
(* |
stmt-id
| *) |
| |
LabelParam of |
(* |
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
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
val mk_logic_label : Cil_types.stmt -> Cil_types.logic_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
.