bap-core-theory
  1. Overview
  2. Docs

The initial theory.

val var : 'a var -> 'a pure

var v is the value of the variable v.

val unk : 'a Value.sort -> 'a pure

unk s an unknown value of sort s.

This term explicitly denotes a term with undefined or unknown value.

val let_ : 'a var -> 'a pure -> 'b pure -> 'b pure

let_ v exp body bind the value of exp to v body.

val ite : bool -> 'a pure -> 'a pure -> 'a pure

ite c x y is x if c evaluates to b1 else y.