MemVal
module type State = sig ... end
module type Value = sig ... end
module Make (_ : Value) : Sigs.Model
module Eva : Value
The glue between WP and EVA. *
Frama-C