Module Builtins.Eval

module NameMatcherMap = Charon.NameMatcher.NameMatcherMap
val match_config : Charon.NameMatcher.match_config
type fixme_fn =
  1. | PanicCleanup
  2. | CatchUnwindCleanup
type optim_fn =
  1. | FloatIs of Soteria.Bv_values.Svalue.FloatClass.t
  2. | FloatIsFinite
  3. | FloatIsSign of {
    1. positive : bool;
    }
  4. | AllocImpl
  5. | Panic
type soteria_fn =
  1. | Assert
  2. | Assume
  3. | NondetBytes
  4. | Panic
type miri_fn =
  1. | Alloc
  2. | AllocId
  3. | Dealloc
  4. | PromiseAlignement
  5. | Nop
type alloc_fn =
  1. | Alloc of {
    1. zeroed : bool;
    }
  2. | Dealloc
  3. | Realloc
  4. | NoAllocShimIsUnstable
type system_fn =
  1. | HashmapRandomKeys
  2. | TlvAtexit
type fn =
  1. | Alloc of alloc_fn
  2. | Fixme of fixme_fn
  3. | Miri of miri_fn
  4. | Optim of optim_fn
  5. | Soteria of soteria_fn
  6. | System of system_fn
  7. | DropInPlace
val std_fun_pair_list : (string * fn) list
val opaque_names : string list
val std_fun_map : fn NameMatcherMap.t
module M (StateM : State.StateM.S) : sig ... end