Module Exec.StartSource

Parameters

module W : Types.WORKLIST

Signature

Sourcetype time = {
  1. mutable sec : float;
}
Sourcemodule Screen : sig ... end
Sourcemodule State : sig ... end
Sourcetype label = [ `Label ] Fiber.t
Sourceand fiber = [ `All ] Fiber.t
Sourceand thunk = {
  1. id : int;
  2. depth : int;
  3. scope : label;
  4. fiber : fiber;
  5. state : State.t;
}
Sourceand 'a mode =
  1. | Default : unit mode
  2. | Linear : State.t mode
  3. | Merge : thunk mode
Sourcetype section =
  1. | RX of {
    1. base : Binsec.Virtual_address.t;
    2. content : Binsec.Loader_buf.t;
    }
  2. | RWX
Sourcetype t = {
  1. mutable code : section Binsec.Imap.t;
    (*

    set of executable sections

    *)
  2. rocache : label Binsec.Virtual_address.Htbl.t;
    (*

    instruction cache for RX sections

    *)
  3. cache : label OMap.t Binsec.Virtual_address.Htbl.t;
    (*

    instruction cache for RWX sections

    *)
  4. mutable worklist : thunk W.t;
    (*

    worklist of pending path

    *)
  5. mutable tid : int;
    (*

    the next unique task identifier

    *)
  6. tasks : unit Libsse.Types.I.Htbl.t;
    (*

    set of tasks to perform

    *)
}
Sourceval env : t
Sourceval choose : unit -> thunk
Sourceval add : thunk -> unit
Sourceval halt : unit -> unit
Sourceexception Continue of label
Sourceval exec : 'a. 'a mode -> int -> int -> max_depth:int -> State.t -> label -> fiber -> 'a
Sourceval assume : 'a. 'a mode -> int -> int -> max_depth:int -> State.t -> label -> [ `Assume ] Fiber.t -> 'a
Sourceval check : 'a. 'a mode -> int -> int -> max_depth:int -> State.t -> label -> [ `Assert ] Fiber.t -> 'a
Sourceval ite : 'a. 'a mode -> int -> int -> max_depth:int -> State.t -> label -> [ `Branch ] Fiber.t -> 'a
Sourceval dynamic_jump : 'a. 'a mode -> int -> int -> max_depth:int -> State.t -> label -> [ `Jump ] Fiber.t -> 'a
Sourceval goto : 'a. 'a mode -> int -> int -> max_depth:int -> State.t -> label -> Binsec.Virtual_address.t -> fiber list -> fiber -> 'a
Sourceval transient_instruction : 'a. 'a mode -> int -> int -> max_depth:int -> State.t -> Binsec.Virtual_address.t -> 'a
Sourceval yield : 'a. 'a mode -> max_depth:int -> 'a
Sourceval probe : 'a. 'a mode -> int -> int -> max_depth:int -> State.t -> label -> [ `Probe ] Fiber.t -> 'a
Sourceval initialize_state : unit -> [ `All ] Fiber.t * State.t