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

module M = M

module L = L

val domain : M.loc Memory.region -> Sigma.Heap.set

Memory footprint of a region.

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

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