package bap-core-theory

an abstract type denoting a Core Theory memory term.

the type of expressions of the target language

an ill-formed term.

store s k x is store (mem s) (bitv k) (bitv x)

store_word d s k x is storew (bool d) (mem s) (bitv k) (bitv x).

var s m n is var (ctxt s) (mems (bits m) (bits n))

unknown m n is unk (mems (bits m) (bits n))

ite c x y is ite (bool c) (mem x) (mem y)

let_bit s x y is scoped @@ fun v -> (bool x) (mem [y|s->v]).

Note, the let_bit rule is not mapped to the let_ term, but instead a scoped fresh variable v is created and s is substituted with v in y.

let_reg s x y is scoped @@ fun v -> (bitv x) (mem [y|s->v]).

Note, the let_reg rule is not mapped to the let_ term, but instead a scoped fresh variable v is created and s is substituted with v in y.

let_mem s x y is scoped @@ fun v -> (mem x) (mem [y|s->v]).

Note, the let_mem rule is not mapped to the let_ term, but instead a scoped fresh variable v is created and s is substituted with v in y.

let_float s x y is scoped @@ fun v -> (float x) (mem [y|s->v]).

Note, the let_float rule is not mapped to the let_ term, but instead a scoped fresh variable v is created and s is substituted with v in y.