package bap-core-theory

  1. Overview
  2. Docs

The denotation of expression.

Values are used to express the semantics of terms that evaluate to a value, aka expressions. Values are sorted and value sorts hold static information about the value representation, like the number of bits in a bitvector or the representation format in a floating point value.

All values belong to the same Knowledge class and thus share the same set of properties, with each property being a specific denotation provided by one or more theories. For example, the bap.std:exp slot holds the denotation of a value in terms of BIL expressions.

type +'a sort

a type for the value sort

type cls

the class of the values.

type 'a t = (cls, 'a sort) KB.cls KB.value

the value type is an instance of Knowledge.value

val cls : (cls, unit) KB.cls

the class of all values.

val empty : 'a sort -> 'a t

empty s creates an empty value of sort s.

The empty value doesn't hold any denotations and represents an absence of information about the value.

val sort : 'a t -> 'a sort

sort v is the value sort.

The value sort holds static information about values of that sort.

module Sort : sig ... end

Value Sorts.