package bap-core-theory

  1. Overview
  2. Docs

The denotation of statements.

An effect is a Knowledge value that is used to give a denotation to the language forms that do not evaluate to values but change the state of the system, i.e., to what is usually called "statement".

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

type +'a sort

a type for the effect sort

type cls

the class of effects.

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

the effect type is an instance of the Knowledge.value

val cls : (cls, unit) KB.cls

the class of all effects.

val empty : 'a sort -> 'a t

empty s creates an empty effect value.

The empty effect denotes an absence of any specific knowledge about the effects produced by a term.

val sort : 'a t -> 'a sort

sort eff returns the sort of the effect eff.

module Sort : sig ... end

Effect sorts.


Innovation. Community. Security.