Frama-C:
Plug-ins:
Libraries:

Frama-C API - P

Relocatable predicate

type t
val pretty : Stdlib.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