sig
  val call :
    adata:Assert.t ->
    loc:Cil_types.location ->
    Cil_types.kernel_function ->
    string ->
    Cil_types.typ ->
    Env.t -> Cil_types.term -> Cil_types.exp * Assert.t * Env.t
  val call_with_size :
    adata:Assert.t ->
    loc:Cil_types.location ->
    Cil_types.kernel_function ->
    string ->
    Cil_types.typ ->
    Env.t ->
    Cil_types.term list ->
    Cil_types.predicate -> Cil_types.exp * Assert.t * Env.t
  val call_valid :
    adata:Assert.t ->
    loc:Cil_types.location ->
    Cil_types.kernel_function ->
    string ->
    Cil_types.typ ->
    Env.t ->
    Cil_types.term -> Cil_types.predicate -> Cil_types.exp * Assert.t * Env.t
  val predicate_to_exp_ref :
    (adata:Assert.t ->
     Cil_types.kernel_function ->
     Env.t -> Cil_types.predicate -> Cil_types.exp * Assert.t * Env.t)
    Stdlib.ref
  val term_to_exp_ref :
    (adata:Assert.t ->
     Cil_types.kernel_function ->
     Env.t -> Cil_types.term -> Cil_types.exp * Assert.t * Env.t)
    Stdlib.ref
  val gmp_to_sizet_ref :
    (adata:Assert.t ->
     loc:Cil_types.location ->
     name:string ->
     ?check_lower_bound:bool ->
     ?pp:Cil_types.term ->
     Cil_types.kernel_function ->
     Env.t -> Cil_types.term -> Cil_types.exp * Assert.t * Env.t)
    Stdlib.ref
end