Module Indpreds

module Indpreds: sig .. end
User-defined inductive predicates


User-defined predicates are ported over from Smallfoot, but do not currently work because of the new assertion normalization implementation.
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;
}
Internal representation of inductive predicates
val add_ip_decl : ip_decl -> unit
Raises Indpred_error if an error occurs
val check_ip_uses : unit -> unit
Raises Indpred_error if an error occurs
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
unroll a node declaration in the lhs
val unroll_node_rhs : Misc.component ->
Exp.exp -> Exp.exp * Exp.exp * Misc.component * Exp.Fld.t * Pure.t
unroll a node declaration in the rhs
Imprint | Data protection