package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Module `CfgCompiler.P`Source

Relocatable predicate

Sourcetype t

Sourceval pretty : Format.formatter -> t -> unit

Sourceval create : Sigma.sigma Node.Map.t -> Lang.F.pred -> t

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

Sourceval get : t -> Lang.F.pred

Sourceval reads : t -> Sigma.domain Node.Map.t

Sourceval nodes : t -> Node.Set.t

Sourceval relocate : Sigma.sigma Node.Map.t -> t -> t

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

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