package frama-c

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module MemBytes.ModelSource

Sourcemodule Chunk = Chunk
Sourcemodule Sigma = Sigma
Sourceval name : string
Sourcetype nonrec loc = loc
Sourceval to_addr : 'a -> 'a
Sourceval to_region_pointer : 'a -> int * 'a
Sourceval of_region_pointer : 'a -> 'b -> 'c -> 'c
Sourceval value_footprint : 'a -> 'b -> Sigma.Chunk.Set.t
Sourceval init_footprint : 'a -> 'b -> Sigma.Chunk.Set.t
Sourceval havoc : Ctypes.c_object -> Lang.F.term -> length:Lang.F.term -> Chunk.t -> fresh:Lang.F.term -> current:Lang.F.term -> Lang.F.term
Sourceval load_pointer : Sigma.t -> 'a -> Lang.F.term -> Lang.F.term
Sourceval store_pointer : Sigma.t -> 'a -> Lang.F.term -> Lang.F.term -> Chunk.t * Lang.F.term
Sourceval set_init : Ctypes.c_object -> Lang.F.term -> length:Lang.F.term -> 'a -> current:Lang.F.term -> Lang.F.term
OCaml

Innovation. Community. Security.