Frama-C API - Model
Loader Model for Atomic Values
module Chunk : Sigs.Chunkmodule Sigma : Sigs.Sigma with type chunk = Chunk.tval sizeof : Ctypes.c_object -> Lang.F.termval field : loc -> Frama_c_kernel.Cil_types.fieldinfo -> locval shift : loc -> Ctypes.c_object -> Lang.F.term -> locConversion among loc, t_pointer terms and t_addr terms
val to_addr : loc -> Lang.F.termval to_region_pointer : loc -> int * Lang.F.termval of_region_pointer : int -> Ctypes.c_object -> Lang.F.term -> locval value_footprint : Ctypes.c_object -> loc -> Sigma.domainval init_footprint : Ctypes.c_object -> loc -> Sigma.domainval frames : Ctypes.c_object -> loc -> Chunk.t -> Sigs.frame listval last : Sigma.t -> Ctypes.c_object -> loc -> Lang.F.termval havoc : Ctypes.c_object -> loc -> length:Lang.F.term -> Chunk.t -> fresh:Lang.F.term -> current:Lang.F.term -> Lang.F.termval eqmem_forall : Ctypes.c_object -> loc -> Chunk.t -> Lang.F.term -> Lang.F.term -> Lang.F.var list * Lang.F.pred * Lang.F.predval load_int : Sigma.t -> Ctypes.c_int -> loc -> Lang.F.termval load_float : Sigma.t -> Ctypes.c_float -> loc -> Lang.F.termval load_pointer : Sigma.t -> Frama_c_kernel.Cil_types.typ -> loc -> locval store_int : Sigma.t -> Ctypes.c_int -> loc -> Lang.F.term -> Chunk.t * Lang.F.termval store_float : Sigma.t -> Ctypes.c_float -> loc -> Lang.F.term -> Chunk.t * Lang.F.termval store_pointer : Sigma.t -> Frama_c_kernel.Cil_types.typ -> loc -> Lang.F.term -> Chunk.t * Lang.F.termval is_init_atom : Sigma.t -> Ctypes.c_object -> loc -> Lang.F.termval is_init_range : Sigma.t -> Ctypes.c_object -> loc -> Lang.F.term -> Lang.F.predval set_init_atom : Sigma.t -> Ctypes.c_object -> loc -> Lang.F.term -> Chunk.t * Lang.F.termval set_init : Ctypes.c_object -> loc -> length:Lang.F.term -> Chunk.t -> current:Lang.F.term -> Lang.F.term