package bap-core-theory

  1. Overview
  2. Docs

Sorts for floating point numbers.

module Format : sig ... end

Sort describing the representation format of a floating point number.

type ('r, 's) format = ('r, 's) Format.t
type 'f t
val define : ('r, 's) format Value.sort -> ('r, 's) format t Value.sort

define r s defines a floating point sort, indexed by the floating point format r that gives the interpretation to the bits of bitvectors of sort s.

val refine : unit Value.sort -> ('r, 's) format t Value.sort option

refine s if s is a floating point sort then restores its type.

val format : ('r, 's) format t Value.sort -> ('r, 's) format Value.sort

format s returns the format of floating points of sort s.

val bits : ('r, 's) format t Value.sort -> 's Bitv.t Value.sort

bits s returns the sort of bitvectors that are used to represent floating point numbers of sort s.

OCaml

Innovation. Community. Security.