Frama-C:
Plug-ins:
Libraries:

Frama-C API - Clabels

Normalized C-labels

Structural representation of logic labels. Compatible with stdlib comparison and structural equality.

type c_label
val is_here : c_label -> bool
val mem : c_label -> c_label list -> bool
val equal : c_label -> c_label -> bool
module T : sig ... end
module LabelMap : Stdlib.Map.S with type key = c_label
module LabelSet : Stdlib.Set.S with type elt = c_label
val pre : c_label
val here : c_label
val next : c_label
val init : c_label
val post : c_label
val exit : c_label
val break : c_label
val continue : c_label
val default : c_label
val loopentry : c_label
val loopcurrent : c_label
val formal : string -> c_label
val case : int64 -> c_label
val stmt_post : Frama_c_kernel.Cil_types.stmt -> c_label
val loop_entry : Frama_c_kernel.Cil_types.stmt -> c_label

Assumes the logic label only comes from normalized or non-ambiguous labels. Ambiguous labels are: Old, LoopEntry and LoopCurrent, since they point to different program points depending on the context.

val is_post : Frama_c_kernel.Cil_types.logic_label -> bool

Checks whether the logic-label is Post or to_logic post

val pretty : Stdlib.Format.formatter -> c_label -> unit

lookup bindings lparam retrieves the actual label for the label in bindings for label parameter lparam.