sig
exception Indpred_error of string * Location.t
type ip_decl = {
ip_id : string;
ip_args : Exp.Id.t list;
ip_body : (Pure.t * Assertions.cform) list;
ip_node : bool;
ip_loc : Location.t;
}
val add_ip_decl : Indpreds.ip_decl -> unit
val check_ip_uses : unit -> unit
val instance_ip_lhs :
string * Exp.exp list -> (Pure.t * Assertions.cform) list
val instance_ip_rhs :
string * Exp.exp list -> (Pure.t * Assertions.cform) list
val init_ip_env : unit -> unit
val print_ip_env : Format.formatter -> unit
val add_ip_use : string * int * Location.t -> unit
val unroll_node_lhs :
Misc.component ->
Exp.exp -> Exp.exp * Exp.exp * Misc.component * Exp.Fld.t * Pure.t
val unroll_node_rhs :
Misc.component ->
Exp.exp -> Exp.exp * Exp.exp * Misc.component * Exp.Fld.t * Pure.t
end