sig
  val t_addr : Lang.F.tau
  val t_malloc : Lang.F.tau
  val t_init : Lang.F.tau
  val t_mem : Lang.F.tau -> Lang.F.tau
  val a_null : Lang.F.term
  val a_global : Lang.F.term -> Lang.F.term
  val a_addr : Lang.F.term -> Lang.F.term -> Lang.F.term
  val a_shift : Lang.F.term -> Lang.F.term -> Lang.F.term
  val a_base : Lang.F.term -> Lang.F.term
  val a_offset : Lang.F.term -> Lang.F.term
  val a_base_offset : Lang.F.term -> Lang.F.term -> Lang.F.term
  val f_null : Lang.lfun
  val f_base : Lang.lfun
  val f_global : Lang.lfun
  val f_shift : Lang.lfun
  val f_offset : Lang.lfun
  val f_havoc : Lang.lfun
  val f_set_init : Lang.lfun
  val f_region : Lang.lfun
  val f_addr_of_int : Lang.lfun
  val f_int_of_addr : Lang.lfun
  val p_addr_lt : Lang.lfun
  val p_addr_le : Lang.lfun
  val p_linked : Lang.lfun
  val p_framed : Lang.lfun
  val p_sconst : Lang.lfun
  val p_cinits : Lang.lfun
  val p_is_init_r : Lang.lfun
  val p_separated : Lang.lfun
  val p_included : Lang.lfun
  val p_valid_rd : Lang.lfun
  val p_valid_rw : Lang.lfun
  val p_valid_obj : Lang.lfun
  val p_invalid : Lang.lfun
  val p_eqmem : Lang.lfun
  val p_monotonic : Lang.lfun
  val register :
    ?base:(Lang.F.term list -> Lang.F.term) ->
    ?offset:(Lang.F.term list -> Lang.F.term) ->
    ?equal:(Lang.F.term -> Lang.F.term -> Lang.F.pred) ->
    ?linear:bool -> Lang.lfun -> unit
  val frames :
    addr:Lang.F.term ->
    offset:Lang.F.term ->
    sizeof:Lang.F.term -> ?basename:string -> Lang.F.tau -> Sigs.frame list
  val separated :
    shift:('-> Ctypes.c_object -> Lang.F.term -> 'a) ->
    addrof:('-> Lang.F.term) ->
    sizeof:(Ctypes.c_object -> Lang.F.term) ->
    'Sigs.rloc -> 'Sigs.rloc -> Lang.F.pred
  val included :
    shift:('-> Ctypes.c_object -> Lang.F.term -> 'a) ->
    addrof:('-> Lang.F.term) ->
    sizeof:(Ctypes.c_object -> Lang.F.term) ->
    'Sigs.rloc -> 'Sigs.rloc -> Lang.F.pred
end