package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

type t
val pretty : Stdlib.Format.formatter -> t -> unit
val create : S.t Sigs.sequence -> Lang.F.pred -> t

Bundle an equation with the sigma sequence that created it

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

as defined by S.writes

val relocate : S.t Sigs.sequence -> t -> t