Module type Sig.With_Boolean
We document the boolean cases, as integer are pretty similar.
module Boolean : Datatype_sig.S with type t = booleanval serialize_boolean :
Context.t ->
boolean ->
Context.t ->
boolean ->
'a Context.in_acc ->
(boolean, 'a) Context.resultEmpty denotes that the concretization has no value (or it is the concrete value representing the absence of value). Note that this does not necessarily imply that some error occured; for instance the offset of an uninitialized pointer can be represented with empty. Emptyness testing is a simple way of communicating between domains.
module Boolean_Forward :
Operator.BOOLEAN_FORWARD
with module Arity := Context_Arity_Forward(Context)
and type boolean := booleanval query_boolean : Context.t -> boolean -> Lattices.Quadrivalent.t