package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

Relocatable predicate

Sourcetype t

Sourceval pretty : Stdlib.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