Frama-C:
Plug-ins:
Libraries:

Frama-C API - E

Relocatable effect (a predicate that depend on two states).

type t
val pretty : Stdlib.Format.formatter -> t -> unit

Bundle an equation with the sigma sequence that created it

val get : t -> Lang.F.pred
val reads : t -> Sigma.domain
val writes : t -> Sigma.domain

as defined by S.writes

val relocate : Sigma.sigma Memory.sequence -> t -> t