package frama-c

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

Relocatable predicate

type t
val pretty : Format.formatter -> t -> unit
val create : S.t Node.Map.t -> Lang.F.pred -> t

Bundle an equation with the sigma sequence that created it. | create m p | = | p |

val get : t -> Lang.F.pred
val reads : t -> S.domain Node.Map.t
val nodes : t -> Node.Set.t
val relocate : S.t Node.Map.t -> t -> t

| relocate m' (create m p) | = | p{ } |

val to_condition : t -> (C.t * Node.t option) option
OCaml

Innovation. Community. Security.