package frama-c

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

Loader Model for Atomic Values

module Chunk : Sigs.Chunk
module Sigma : Sigs.Sigma with type chunk = Chunk.t
val name : string
type loc
val shift : loc -> Ctypes.c_object -> Lang.F.term -> loc

Conversion among loc, t_pointer terms and t_addr terms

val to_addr : loc -> Lang.F.term
val to_region_pointer : loc -> int * Lang.F.term
val of_region_pointer : int -> Ctypes.c_object -> Lang.F.term -> loc
val value_footprint : Ctypes.c_object -> loc -> Sigma.domain
val init_footprint : Ctypes.c_object -> loc -> Sigma.domain
val frames : Ctypes.c_object -> loc -> Chunk.t -> Sigs.frame list
val havoc : Ctypes.c_object -> loc -> length:Lang.F.term -> Chunk.t -> fresh:Lang.F.term -> current:Lang.F.term -> Lang.F.term
val load_int : Sigma.t -> Ctypes.c_int -> loc -> Lang.F.term
val load_float : Sigma.t -> Ctypes.c_float -> loc -> Lang.F.term
val load_pointer : Sigma.t -> Frama_c_kernel.Cil_types.typ -> loc -> loc
val store_int : Sigma.t -> Ctypes.c_int -> loc -> Lang.F.term -> Chunk.t * Lang.F.term
val store_float : Sigma.t -> Ctypes.c_float -> loc -> Lang.F.term -> Chunk.t * Lang.F.term
val is_init_atom : Sigma.t -> loc -> Lang.F.term
val is_init_range : Sigma.t -> Ctypes.c_object -> loc -> Lang.F.term -> Lang.F.pred
val set_init_atom : Sigma.t -> loc -> Lang.F.term -> Chunk.t * Lang.F.term
val set_init : Ctypes.c_object -> loc -> length:Lang.F.term -> Chunk.t -> current:Lang.F.term -> Lang.F.term