Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package bap-core-theory
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Sorts of memories.
A memory is an associative container of bitvectors indexed with bitvector keys.
val define :
'a Bitv.t Value.sort ->
'b Bitv.t Value.sort ->
('a, 'b) t Value.sortdefine ks vs a sort of memories with keys of type ks and data of type vs.
val refine : unit Value.sort -> ('a, 'b) t Value.sort optionrefine s if s is a memory sort then restores its type.
val keys : ('a, 'b) t Value.sort -> 'a Bitv.t Value.sortkeys s returns the sort of keys.
val vals : ('a, 'b) t Value.sort -> 'b Bitv.t Value.sortvals s returns the sort of values.