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

module M : Sigs.Model

module L : Sigs.LogicSemantics with module M = M

Sourcemodule M = M

Sourcemodule L = L

Sourceval domain : M.loc Sigs.region -> M.Heap.set

Memory footprint of a region.

val apply_assigns : 
  M.sigma Sigs.sequence ->
  M.loc Sigs.region ->
  Lang.F.pred list

Relates two memory states corresponding to an assigns clause with the specified set of locations.

On This Page