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