Parameter Make._

val name : string

Name of the inductive predicate.

val signature : Sort.t list
val default_instantiation : MemoryModel.StructDef.t list
val instantiate : HeapSort.t -> Sort.t list -> (MemoryModel.StructDef.t list, string) Stdlib.Result.t

Check whether ID can be instantiated with variables of given sorts. If true, return a list of structures describing this instance. Otherwise, return a message decsribing why such instantiation is not possible.

val must_allocated : SL.Term.t list -> SL.Term.t list
val unique_footprint : bool

True iff the predicate has unique footprint.

val struct_defs : MemoryModel.StructDef.t list
val heap_sort : HeapSort.t
val term_bound : SL.t -> HeapSort.t -> SL.Term.t -> float
val sl_graph : ID_sig.instance -> SL_graph0.t
val additional_bound : SL.t -> LocationBounds0.t
val rules : (SL.Variable.t list * MemoryModel.StructDef.t list) -> SL.t list
val global_preprocessing : SL.t -> SL.t
module Bound : sig ... end
module Translation (E : Translation_sig.ENCODING) : sig ... end

Preprocessing

val preprocess : SL_graph0.t -> SL.Term.t list -> SL.t option

Model checking

val model_check : ID_sig.instance -> StackHeapModel.t -> bool