package frama-c

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

Generates Loader for Compound Values

Parameters

module M : Model

Signature

val load_init : M.Sigma.t -> Ctypes.c_object -> M.loc -> Lang.F.term
val load_value : M.Sigma.t -> Ctypes.c_object -> M.loc -> Lang.F.term
val copied_init : M.Sigma.t Sigs.sequence -> Ctypes.c_object -> M.loc -> M.loc -> Sigs.equation list
val initialized : M.Sigma.t -> M.loc Sigs.rloc -> Lang.F.pred