In this paper we present an approach to check resource consumption contracts using an off-the-shelf static analyzer. We propose a set of annotations to support resource usage specifications, in particular, dynamic memory consumption constraints. Since dynamic memory may be recycled by a memory manager, the consumption of this resource is not monotone. The specification language can express both memory consumption and lifetime properties in a modular fashion. We develop a proof-of-concept implementation by extending Code Contracts' specification language. To verify the correctness of these annotations we rely on the Code Contracts static verifier and a points-to analysis. We also briefly discuss possible extensions of our approach to deal with non-linear expressions.
@article{arxiv.1401.0968,
title = {On Verifying Resource Contracts using Code Contracts},
author = {Rodrigo Castaño and Juan Pablo Galeotti and Diego Garbervetsky and Jonathan Tapicer and Edgardo Zoppi},
journal= {arXiv preprint arXiv:1401.0968},
year = {2014}
}