Module Simple_memory

module Simple_memory: sig .. end

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_bottom 

A 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).

module type Value = sig .. end

Abstraction of the values variables are mapped to.

module type S = sig .. end

Signature of a simple memory abstraction for scalar variables.

module Make_Memory: 
functor (Value : Value-> sig .. end
module Make_Domain: 
functor (Info : sig
val name : string
end-> 
functor (Value : Value-> sig .. end