module PrintBTL:sig..end
BTL instruction printer
val print_aaddr_annot_opt : bool Stdlib.ref
val print_sval_hashcode_opt : bool Stdlib.ref
val print_list : ?sep:(Stdlib.out_channel -> unit) ->
(Stdlib.out_channel -> 'a -> unit) -> Stdlib.out_channel -> 'a list -> unit
val reg : Stdlib.out_channel -> Camlcoq.P.t -> unit
val regs : Stdlib.out_channel -> Camlcoq.P.t list -> unit
val ros : Stdlib.out_channel -> (Camlcoq.P.t, Camlcoq.atom) Datatypes.sum -> unit
val print_succ : Stdlib.out_channel -> Camlcoq.P.t -> unit
val print_pref : Stdlib.out_channel -> string -> unit
val print_aaddr : Stdlib.out_channel -> ValueDomain.aval option -> unit
val print_store_num : Stdlib.out_channel -> BTL_Invariants.store_num_t -> unit
val print_store_info : Stdlib.out_channel -> BTL_Invariants.store_info -> unit
val print_sgn : Stdlib.out_channel -> bool -> unit
val print_prom_sgns : Stdlib.out_channel -> 'a option * 'b option -> unit
val print_inst_info : Stdlib.out_channel -> BTL.inst_info * Camlcoq.P.t list -> unit
val print_iblock : Stdlib.out_channel -> bool -> string -> BTL.iblock -> unit
val print_btl_inst : Stdlib.out_channel -> BTL.iblock -> unit
val print_btl_block : Stdlib.out_channel -> BTL.iblock_info -> Camlcoq.P.t -> unit
val sort_elts : 'a Maps.PTree.t -> (BinNums.positive * 'a) list
val print_btl_code : Stdlib.out_channel -> BTL.iblock_info Maps.PTree.t -> unit
val destination : string option Stdlib.ref
val print_if : Camlcoq.Z.t -> BTL.iblock_info Maps.PTree.t -> unit
val print_ireg : Stdlib.out_channel -> BTL_Invariants.ireg -> unit
val print_ireg_list : Stdlib.out_channel -> BTL_Invariants.ireg list -> unit
val print_rop : Stdlib.out_channel -> BTL_Invariants.root_op * Camlcoq.P.t list -> unit
val lir_to_lr : BTL_Invariants.ireg list -> Registers.reg list
val print_ival : Stdlib.out_channel -> BTL_Invariants.ival -> unit
val print_istore : Stdlib.out_channel -> BTL_Invariants.istore -> unit
val print_imem : Stdlib.out_channel -> BTL_Invariants.istore list -> unit
val lsval_length : BTL_Invariants.list_sval -> int
val fake_args : BTL_Invariants.list_sval -> Camlcoq.P.t list
val print_sval_hc : Stdlib.out_channel -> int -> unit
val name_of_permission : Memtype.permission -> string
val print_sval : Stdlib.out_channel -> BTL_Invariants.sval -> unit
val print_lsval : Stdlib.out_channel -> BTL_Invariants.list_sval -> unit
val print_smem : Stdlib.out_channel -> BTL_Invariants.smem -> unit
val print_okclause : Stdlib.out_channel -> BTL_Invariants.okclause -> unit
val print_list_sval : Stdlib.out_channel -> BTL_Invariants.sval list -> unit
val print_sreg : BTL_Invariants.sval Maps.PTree.t -> unit
val print_option : (Stdlib.out_channel -> 'a -> unit) -> Stdlib.out_channel -> 'a option -> unit
val print_sstate : BTL_SEsimuref.ristate -> unit
val print_sstates : BTL_SEsimuref.ristate -> BTL_SEsimuref.ristate -> unit
val print_csasv : Stdlib.out_channel -> string -> BTL_Invariants.csasv -> unit
val print_invariant : Stdlib.out_channel -> BTL_Invariants.invariants -> unit
val print_gluemap : BTL_Invariants.invariants Maps.PTree.t -> unit
module PrintGV:sig..end