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:
module Make_Domain: