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=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

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

Sourcetype t

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

Sourceval create : S.t Sigs.sequence -> Lang.F.pred -> t

Bundle an equation with the sigma sequence that created it

Sourceval get : t -> Lang.F.pred

Sourceval reads : t -> S.domain

Sourceval writes : t -> S.domain

as defined by S.writes

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