package frama-c

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Chunk = Chunk
module Sigma = Sigma
val name : string
type nonrec loc = loc
val to_addr : 'a -> 'a
val to_region_pointer : 'a -> int * 'a
val of_region_pointer : 'a -> 'b -> 'c -> 'c
val value_footprint : 'a -> 'b -> Sigma.Chunk.Set.t
val init_footprint : 'a -> 'b -> Sigma.Chunk.Set.t
val havoc : Ctypes.c_object -> Lang.F.term -> length:Lang.F.term -> Chunk.t -> fresh:Lang.F.term -> current:Lang.F.term -> Lang.F.term
val load_pointer : Sigma.t -> 'a -> Lang.F.term -> Lang.F.term
val store_pointer : Sigma.t -> 'a -> Lang.F.term -> Lang.F.term -> Chunk.t * Lang.F.term
val is_init_atom : Sigma.t -> Ctypes.c_object -> Lang.F.term -> Lang.F.term
val set_init : Ctypes.c_object -> Lang.F.term -> length:Lang.F.term -> 'a -> current:Lang.F.term -> Lang.F.term
OCaml

Innovation. Community. Security.