package frama-c

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

Module Wp.ClabelsSource

Normalized C-labels

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

Sourcetype c_label
Sourceval is_here : c_label -> bool
Sourceval mem : c_label -> c_label list -> bool
Sourceval equal : c_label -> c_label -> bool
Sourcemodule T : sig ... end
Sourcemodule LabelMap : Map.S with type key = c_label
Sourcemodule LabelSet : Set.S with type elt = c_label
Sourceval pre : c_label
Sourceval here : c_label
Sourceval next : c_label
Sourceval init : c_label
Sourceval post : c_label
Sourceval exit : c_label
Sourceval break : c_label
Sourceval continue : c_label
Sourceval default : c_label
Sourceval loopentry : c_label
Sourceval loopcurrent : c_label
Sourceval formal : string -> c_label
Sourceval case : int64 -> c_label
Sourceval stmt_post : Frama_c_kernel.Cil_types.stmt -> c_label
Sourceval 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.

Sourceval is_post : Frama_c_kernel.Cil_types.logic_label -> bool

Checks whether the logic-label is Post or to_logic post

Sourceval 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