package frama-c

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Wp.FootprintSource

Term Footprints

Sourceval iter : (Lang.F.term -> unit) -> Lang.F.term -> unit

Width-first full iterator.

Sourceval once : (Lang.F.term -> unit) -> Lang.F.term -> unit

Width-first once iterator.

Sourceval head : Lang.F.term -> string

Head only footprint

Sourceval pattern : Lang.F.term -> string

Generate head footprint up to size

Sourceval matches : string -> Lang.F.term -> bool

Head match

Sourcetype occurrence = int * string

k-th occurrence of the footprint in a term

Sourceval locate : select:Lang.F.term -> inside:Lang.F.term -> occurrence

Locate the occurrence of select footprint inside a term.

Sourceval lookup : occur:occurrence -> inside:Lang.F.term -> Lang.F.term

Retrieve back the k-th occurrence of a footprint inside a term.

OCaml

Innovation. Community. Security.