package encoding

  1. Overview
  2. Docs

Module Encoding.ExprSource

Term definitions of the abstract syntax

Sourcetype t = {
  1. e : expr;
  2. ty : Ty.t;
}
Sourceand expr =
  1. | Val of Value.t
  2. | Ptr of int32 * t
  3. | Unop of Ty.unop * t
  4. | Binop of Ty.binop * t * t
  5. | Triop of Ty.triop * t * t * t
  6. | Relop of Ty.relop * t * t
  7. | Cvtop of Ty.cvtop * t
  8. | Symbol of Symbol.t
  9. | Extract of t * int * int
  10. | Concat of t * t
Sourceval v : expr -> Ty.t -> t
Sourceval (@:) : expr -> Ty.t -> t
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
Sourceval mk_symbol : Symbol.t -> t
Sourceval get_symbols : t list -> Symbol.t list
Sourceval negate_relop : t -> (t, string) Result.t
Sourceval pp : Format.formatter -> t -> unit
Sourceval pp_smt : Format.formatter -> t list -> unit
Sourceval pp_list : Format.formatter -> t list -> unit
Sourceval to_string : t -> string
Sourceval simplify : ?extract:bool -> t -> t
Sourcemodule Bitv : sig ... end
OCaml

Innovation. Community. Security.