Frama-C API - Simple_memory
Simple memory abstraction for scalar non-volatile variables, built upon a value abstraction. Basically a map from variable to values.
type 'value builtin = 'value list -> 'value Eval.or_bottomA builtin is an ocaml function for the interpretation of a whole C function: it takes the list of value arguments, and returns the result (that can be bottom).
type widen_hint = Frama_c_kernel.Z.Set.t * Frama_c_kernel.Datatype.Float.Set.tSet of relevant thresholds for the widening.
module type Value = sig ... endAbstraction of the values variables are mapped to.
module type S = sig ... endSignature of a simple memory abstraction for scalar variables.
module Make_Memory (_ : sig ... end) (Value : Value) : sig ... endmodule Make_Domain (_ : sig ... end) (Value : Value) : sig ... end