Frama-C:
Plug-ins:
Libraries:

Frama-C API - Footprint

Term Footprints

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

Width-first full iterator.

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

Width-first once iterator.

val head : Lang.F.term -> string

Head only footprint

val pattern : Lang.F.term -> string

Generate head footprint up to size

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

Head match

type occurrence = int * string

k-th occurrence of the footprint in a term

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

Locate the occurrence of select footprint inside a term.

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

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