package frama-c

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

Compiler for Performing Assigns

module M : Model
module L : LogicSemantics with module M = M
val domain : M.loc region -> M.Heap.set

Memory footprint of a region.

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

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