module Abstraction: sig .. end
Shape-value abstraction of assertions
This module implements shape-value abstraction, which includes an adaptation
of Distefano's simple list segment domain and custom abstractions for
possibly sorted sequences and multiset values.
References:
- Vafeiadis, V.: Shape-value abstraction for verifying linearizability.
In: Jones, N.D., Mueller-Olm, M. (eds.) VMCAI 2009.
LNCS, vol. 5403, pp. 335-348. Springer, Heidelberg (2009)
- Distefano, D., O'Hearn, P.W., Yang, H.: A local shape analysis based
on separation logic. In: Hermsnnd, H., Palsberg, J. (eds.) TACAS 2006.
LNCS, vol. 3920, pp. 287-302. Springer, Heidelberg (2006)
type
val add_imp_vars : string -> unit
val add_sorted_from : string -> unit
val default_options : abs_options
val sorting_options : abs_options
val valB_options : abs_options
val valA_valB_options : abs_options
val mk_abstraction : abs_options -> Assertions.prover -> Genarith.abstraction
Main entry point.
val prover_calls : int Pervasives.ref
Number of calls to the theorem prover during abstraction
val verbose : int Pervasives.ref
val args : (Arg.key * Arg.spec * Arg.doc) list