bap-core-theory 2.1.0 · OCaml Package

Statements.

type t

an abstract type denoting effects of the Core Theory.

type exp

the type of expressions of the target language.

type rmode

the type for representing rounding modes in the target language.

type stmt

the type of statements in the target language.

val error : t

an ill-formed term.

val set_mem : string -> int -> int -> exp -> t

set_mem s m n x is set v (mem x),

where v = Var.create (mems (bits m) (bits n) s.

val set_reg : string -> int -> exp -> t

set_reg s m x is set v (bitv x),

where v = Var.create (bits m) s.

val set_bit : string -> exp -> t

set_bit s x is set v (bool x),

where v = Var.create Bool.t s.

val set_ieee754 : string -> ieee754 -> exp -> t

set_ieee754 s p x is set v (float x),

where v = Var.create (IEEE754.Sort.define p) s.

val set_rmode : string -> rmode -> t

set_rmode s x is set v (rmode x),

where v = Var.create Rmode.t x.

val tmp_mem : string -> exp -> t

tmp_mem s x is set v (mem x),

where v is a freshly created variable, and all occurrences of s are substituted with the identifier of v in all subsequent statements.

val tmp_reg : string -> exp -> t

tmp_reg s x is set v (bitv x),

where v is a freshly created variable, and all occurrences of s are substituted with the identifier of v in all subsequent statements.

val tmp_bit : string -> exp -> t

tmp_bit s x is set v (bool x),

where v is a freshly created variable, and all occurrences of s are substituted with the identifier of v in all subsequent statements.

val tmp_float : string -> exp -> t

tmp_float s x is set v (float x),

where v is a freshly created variable, and all occurrences of s are substituted with the identifier of v in all subsequent statements.

val tmp_rmode : string -> rmode -> t

tmp_rmode s x is set v (rmode x),

where v is a freshly created variable, and all occurrences of s are substituted with the identifier of v in all subsequent statements.

val let_mem : string -> exp -> stmt -> t

let_mem s x p is seq (set v (mem x)) (stmt p),