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