package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 : Map.S with type key = c_label
module LabelSet : 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 points to different program points dependending 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 : Format.formatter -> c_label -> unit

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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct